summaryrefslogtreecommitdiff
path: root/Build/source/Build
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2016-03-16 22:51:11 +0000
committerKarl Berry <karl@freefriends.org>2016-03-16 22:51:11 +0000
commitd1e6851ad63caca1829a5a975071721c6b2b7c56 (patch)
tree4922c1678a5d69ec31532c849cae5772f1da415a /Build/source/Build
parent4c11a739919c6fe82bd1e3890115da2a7b447bee (diff)
check for exitstatus.txt not having an exit status
git-svn-id: svn://tug.org/texlive/trunk@40049 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Build/source/Build')
-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