diff options
| author | Gaëtan Gilbert | 2018-03-09 14:05:36 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-31 00:58:15 +0200 |
| commit | aa1565a20f6c42ba28a9346ee25404d893946c5d (patch) | |
| tree | fce245a4f7d2205e859b460459306de9f3b3e283 /dev | |
| parent | d4def32456c0fadb7fc9814af7e7b2b21a37f0a6 (diff) | |
Linter: verify overlay extensions.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/lint-repository.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index ee9c8777a3..cd09b6d305 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -31,4 +31,6 @@ fi find . "(" -path ./.git -prune ")" -o -type f -print0 | xargs -0 dev/tools/check-eof-newline.sh || CODE=1 +dev/tools/check-overlays.sh || CODE=1 + exit $CODE |