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