summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xBuild/source/Build4
1 files changed, 4 insertions, 0 deletions
diff --git a/Build/source/Build b/Build/source/Build
index 2389a106968..642ad3e8ba9 100755
--- a/Build/source/Build
+++ b/Build/source/Build
@@ -150,6 +150,10 @@ if test -d "$bindir"; then
fi
status=`cat exitstatus.txt`
+if echo "$status | egrep '^[0-9]+$' >/dev/null; then :; else
+ echo "$0: exitstatus.txt does not contain a number; disk full?" >&2
+ status=1
+fi
echo "done (exit status $status)" `date` | tee -a build.log
exit $status