equal
deleted
inserted
replaced
5 # |
5 # |
6 # Isabelle interface startup script. |
6 # Isabelle interface startup script. |
7 |
7 |
8 if [ -L "$0" ]; then |
8 if [ -L "$0" ]; then |
9 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
9 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
10 exec $(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET") "$@" |
10 exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
11 fi |
11 fi |
12 |
12 |
13 |
13 |
14 ## settings |
14 ## settings |
15 |
15 |