diff options
| -rwxr-xr-x | Build/source/Build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Build/source/Build b/Build/source/Build index 642ad3e8ba9..1cc955f83d5 100755 --- a/Build/source/Build +++ b/Build/source/Build @@ -150,7 +150,7 @@ if test -d "$bindir"; then fi status=`cat exitstatus.txt` -if echo "$status | egrep '^[0-9]+$' >/dev/null; then :; else +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 |