equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # Author: Markus Wenzel, TU Muenchen |
3 # Author: Markus Wenzel, TU Muenchen |
4 # |
4 # |
5 # Isabelle tool wrapper. |
5 # Isabelle tool wrapper. |
|
6 |
|
7 unset CDPATH |
6 |
8 |
7 if [ -L "$0" ]; then |
9 if [ -L "$0" ]; then |
8 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
10 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
9 exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
11 exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
10 fi |
12 fi |