changeset 15784 | 3a214de33d53 |
parent 15779 | aed221aff642 |
child 15801 | d2f5ca3c048d |
--- a/bin/isabelle-process Wed Apr 20 18:57:05 2005 +0200 +++ b/bin/isabelle-process Wed Apr 20 19:00:30 2005 +0200 @@ -17,7 +17,7 @@ while [ -L "$THIS" ]; do THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')" done -ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)" +ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)" . "$ISABELLE_HOME/lib/scripts/getsettings" || \ { echo "$PRG probably not called from its original place!"; exit 2; }