bin/isabelle
changeset 2936 bd33e7aae062
parent 2768 bc6d915b8019
child 2968 8ba30b031f31
     1.1 --- a/bin/isabelle	Fri Apr 11 15:21:36 1997 +0200
     1.2 +++ b/bin/isabelle	Fri Apr 11 17:30:15 1997 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  ISABELLE_HOME=$(dirname $0)/..
     1.6  . $ISABELLE_HOME/lib/scripts/getsettings || \
     1.7 -  { echo "$PRG probably not called from its original place!"; exit 2 }
     1.8 +  { echo "$PRG probably not called from its original place!"; exit 2; }
     1.9  
    1.10  
    1.11  ## diagnostics
    1.12 @@ -104,7 +104,7 @@
    1.13    shift
    1.14  fi
    1.15  
    1.16 -[ $# -ne 0 ] && { echo "Bad args: $*"; usage }
    1.17 +[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
    1.18  
    1.19  
    1.20  ## check ML system