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
Merged

Fix lint filter against deleted files. Fixes #563#564
kroening merged 1 commit intodiffblue:masterfrom
smowton:fix_filter_lint_deleted_files

Commits

Commits on Feb 21, 2017