| changeset 10511 | efb3428c9879 |
| parent 9786 | 270ca580b880 |
| child 10555 | 2323ec838401 |
--- a/bin/isatool Wed Nov 22 21:38:26 2000 +0100 +++ b/bin/isatool Wed Nov 22 21:41:39 2000 +0100 @@ -10,9 +10,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; }