Merge pull request #564 from smowton/fix_filter_lint_deleted_files

Fix lint filter against deleted files. Fixes #563

Author: Daniel Kroening

scripts/filter_lint_by_diff.py

@@ -15,6 +15,9 @@
   diff = unidiff.PatchSet(f)
   for diff_file in diff:
     filename = diff_file.target_file
+    # Skip files deleted in the tip (b side of the diff):
+    if filename == "/dev/null":
+      continue
     assert filename.startswith("b/")
     filename = os.path.join(repository_root, filename[2:])
     added_lines.add((filename, 0))