equal
deleted
inserted
replaced
3 # $Id$ |
3 # $Id$ |
4 # Author: Markus Wenzel, TU Muenchen |
4 # Author: Markus Wenzel, TU Muenchen |
5 # |
5 # |
6 # Isabelle tool starter -- provides settings environment |
6 # Isabelle tool starter -- provides settings environment |
7 # and keeps your PATH name space clean. |
7 # and keeps your PATH name space clean. |
|
8 |
|
9 if [ -L "$0" ]; then |
|
10 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
|
11 exec $(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET") "$@" |
|
12 fi |
8 |
13 |
9 |
14 |
10 ## settings |
15 ## settings |
11 |
16 |
12 PRG="$(basename "$0")" |
17 PRG="$(basename "$0")" |