diff -r 998cb95fdd43 -r bd33e7aae062 build
--- a/build	Fri Apr 11 15:21:36 1997 +0200
+++ b/build	Fri Apr 11 17:30:15 1997 +0200
@@ -11,7 +11,7 @@
 
 ISABELLE_HOME=$(dirname $0)
 . $ISABELLE_HOME/lib/scripts/getsettings || \
-  { echo "$PRG probably not called from its original place!"; exit 2 }
+  { echo "$PRG probably not called from its original place!"; exit 2; }
 
 
 ## diagnostics