changeset 15784 | 3a214de33d53 |
parent 15778 | 98af3693f6b3 |
child 15843 | d5bd4a18ce70 |
--- a/bin/isabelle Wed Apr 20 18:57:05 2005 +0200 +++ b/bin/isabelle Wed Apr 20 19:00:30 2005 +0200 @@ -9,7 +9,7 @@ while [ -L "$THIS" ]; do THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')" done -THIS="$(cd "$(dirname "$(readlink -f "$THIS")")"; pwd)" +THIS="$(cd "$(dirname "$THIS")"; pwd)" NAME="$(basename "$0")" case "$NAME" in