diff options
-rwxr-xr-x | Build/source/Build | 4 |
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 |