diff options
Diffstat (limited to 'tools/check-tree.sh')
| -rwxr-xr-x | tools/check-tree.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/check-tree.sh b/tools/check-tree.sh index c3aaa08d..e3ddf8bd 100755 --- a/tools/check-tree.sh +++ b/tools/check-tree.sh @@ -68,6 +68,7 @@ if [ "${#SHELL_TESTS[@]}" -eq 0 ] ; then fi for t in "${SHELL_TESTS[@]}" ; do check_shell_dumps "$t" + head -n 1 "$t" |grep -q '^#!/bin/sh' && echo "$t uses sh instead of bash" && EXIT_CODE=1 done ############################################################################## |