diff options
Diffstat (limited to 'src/etc/tidy.py')
| -rw-r--r-- | src/etc/tidy.py | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/etc/tidy.py b/src/etc/tidy.py index f042728b462..b46a6fd8391 100644 --- a/src/etc/tidy.py +++ b/src/etc/tidy.py @@ -18,7 +18,8 @@ def report_err(s): print("%s:%d: %s" % (fileinput.filename(), fileinput.filelineno(), s)) err=1 -file_names = [s for s in sys.argv[1:] if not s.endswith("_gen.rs")] +file_names = [s for s in sys.argv[1:] if (not s.endswith("_gen.rs")) + and (not s.startswith(".#"))] try: for line in fileinput.input(file_names, |