Skip to content

Fix lint filter against deleted files. Fixes #563#564

Merged
kroening merged 1 commit intodiffblue:masterfrom
smowton:fix_filter_lint_deleted_files
Feb 21, 2017

Commits

Commits on Feb 21, 2017