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