bin/isatool
changeset 2936 bd33e7aae062
parent 2787 33931e1023e3
child 3007 e5efa177ee0c
     1.1 --- a/bin/isatool	Fri Apr 11 15:21:36 1997 +0200
     1.2 +++ b/bin/isatool	Fri Apr 11 17:30:15 1997 +0200
     1.3 @@ -12,7 +12,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