diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-07-16 09:28:56 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-07-16 09:29:17 -0400 |
| commit | 6bf19130203c83bb72dd20a5c1ccd99a6716cb3b (patch) | |
| tree | 3ae04926b71e64e0db99ff2897501ac04980b0aa | |
| parent | e27d2fd32e40937e48889772361f1cf53dd9c48e (diff) | |
Only check overlay extensions on git-tracked files
This way, when editors leave over temporary files from editing
user-overlays, we don't prevent commits unless they are added to git.
| -rwxr-xr-x | dev/tools/check-overlays.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh index f7e05b51c..33a9ff058 100755 --- a/dev/tools/check-overlays.sh +++ b/dev/tools/check-overlays.sh @@ -1,8 +1,8 @@ #!/usr/bin/env bash -for f in dev/ci/user-overlays/* +for f in $(git ls-files "dev/ci/user-overlays/") do - if ! ([[ $f = dev/ci/user-overlays/README.md ]] || [[ $f == *.sh ]]) + if ! ([[ "$f" = dev/ci/user-overlays/README.md ]] || [[ "$f" == *.sh ]]) then >&2 echo "Bad overlay '$f'." >&2 echo "User overlays need to have extension .sh to be picked up!" |