diff options
Diffstat (limited to 'Build/source/Build')
-rwxr-xr-x | Build/source/Build | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Build/source/Build b/Build/source/Build index 9572ca0937f..76d72dc539c 100755 --- a/Build/source/Build +++ b/Build/source/Build @@ -124,6 +124,7 @@ if test -d "$bindir"; then # Any errors will have been duly reported anyway. fi -echo done `date` | tee -a build.log +status=`cat exitstatus.txt` +echo "done (exit status $status)" `date` | tee -a build.log -exit `cat exitstatus.txt` +exit $status |