| changeset 10511 | efb3428c9879 |
| parent 10104 | cf49932f3c42 |
| child 10555 | 2323ec838401 |
--- a/bin/isabelle Wed Nov 22 21:38:26 2000 +0100 +++ b/bin/isabelle Wed Nov 22 21:41:39 2000 +0100 @@ -9,9 +9,9 @@ ## settings -PRG=$(basename "$0") +PRG="$(basename "$0")" -ISABELLE_HOME=$(dirname "$0")/.. +ISABELLE_HOME="$(dirname "$0")/.." . "$ISABELLE_HOME/lib/scripts/getsettings" || \ { echo "$PRG probably not called from its original place!"; exit 2; }