--- 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