Closes 31679.
@@ -31,6 +31,7 @@ TOPLEVEL=$(dirname "$(dirname "$HERE")")
if [ ! -d "$TOPLEVEL/src" ]; then
printf "Error: Couldn't find src directory in expected location: %s\\n" \
"$TOPLEVEL/src"
+ exit 1
fi
# Check *.sh scripts, but ignore the ones that we can't fix