diff --git a/TOOLS/checktree.sh b/TOOLS/checktree.sh index 433f1ed8b1..eff1fa5b07 100755 --- a/TOOLS/checktree.sh +++ b/TOOLS/checktree.sh @@ -172,7 +172,7 @@ for i in "$@"; do disable_all_tests ;; -none) - disable_all + disable_all_tests ;; -*) echo "unknown option: $i" >&2