diff options
Diffstat (limited to '.gitlab/linters/check-cpp.py')
| -rwxr-xr-x | .gitlab/linters/check-cpp.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitlab/linters/check-cpp.py b/.gitlab/linters/check-cpp.py index 5377fcb005..1b4b26a760 100755 --- a/.gitlab/linters/check-cpp.py +++ b/.gitlab/linters/check-cpp.py @@ -29,6 +29,8 @@ for l in linters: # Don't lint font files l.add_path_filter(lambda path: not path.parent == Path('docs','users_guide', 'rtd-theme', 'static', 'fonts')) + # Don't lint core spec + l.add_path_filter(lambda path: not path.name == 'core-spec.pdf') if __name__ == '__main__': run_linters(linters) |