diff options
| author | Gaëtan Gilbert | 2018-03-09 13:59:17 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-31 00:58:15 +0200 |
| commit | d4def32456c0fadb7fc9814af7e7b2b21a37f0a6 (patch) | |
| tree | 40c7cb812e1cb2073f1d02d6ad44725555da04ff /dev/tools/pre-commit | |
| parent | c0eedb5bdcb815132f404e19d6bf59730ae6e2df (diff) | |
pre-commit: verify user overlay extensions (must be .sh).
This has come up a couple times.
Diffstat (limited to 'dev/tools/pre-commit')
| -rwxr-xr-x | dev/tools/pre-commit | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index c9cdee84ab..a514b8866a 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -5,6 +5,8 @@ set -e +dev/tools/check-overlays.sh + if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh || ! git diff-index --check --cached HEAD >/dev/null 2>&1 ; then |