bin/isatool

--- a/bin/isatool	Fri Apr 11 15:21:36 1997 +0200
+++ b/bin/isatool	Fri Apr 11 17:30:15 1997 +0200
@@ -12,7 +12,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