bin/isabelle
changeset 2936 bd33e7aae062
parent 2768 bc6d915b8019
child 2968 8ba30b031f31
--- a/bin/isabelle	Fri Apr 11 15:21:36 1997 +0200
+++ b/bin/isabelle	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
@@ -104,7 +104,7 @@
   shift
 fi
 
-[ $# -ne 0 ] && { echo "Bad args: $*"; usage }
+[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
 
 
 ## check ML system