diff options
author | Karl Berry <karl@freefriends.org> | 2016-03-16 22:51:11 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2016-03-16 22:51:11 +0000 |
commit | d1e6851ad63caca1829a5a975071721c6b2b7c56 (patch) | |
tree | 4922c1678a5d69ec31532c849cae5772f1da415a | |
parent | 4c11a739919c6fe82bd1e3890115da2a7b447bee (diff) |
check for exitstatus.txt not having an exit status
git-svn-id: svn://tug.org/texlive/trunk@40049 c570f23f-e606-0410-a88d-b1316a301751
-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 |