diff options
Diffstat (limited to '.gitlab')
| -rwxr-xr-x | .gitlab/linters/check-makefiles.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab/linters/check-makefiles.py b/.gitlab/linters/check-makefiles.py index b647f6c1c5..19b7b56368 100755 --- a/.gitlab/linters/check-makefiles.py +++ b/.gitlab/linters/check-makefiles.py @@ -13,7 +13,7 @@ from linter import run_linters, RegexpLinter linters = [ RegexpLinter(r'--interactive', message = "Warning: Use `$(TEST_HC_OPTS_INTERACTIVE)` instead of `--interactive -ignore-dot-ghci -v0`." - ).add_path_filter(lambda path: path.suffix == '.T') + ).add_path_filter(lambda path: path.name == 'Makefile') ] if __name__ == '__main__': |