diff -r 73cf5ef8ed20 -r f9163c6f69d6 bin/isabelle --- a/bin/isabelle Tue May 17 01:24:19 2005 +0200 +++ b/bin/isabelle Tue May 17 09:58:40 2005 +0200 @@ -7,10 +7,10 @@ if [ -L "$0" ]; then TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" - exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" + exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" fi -THIS=$(cd "$(dirname "$0")"; pwd) +THIS=$(cd "$(dirname "$0")"; pwd -P) NAME="$(basename "$0")" case "$NAME" in