equal
deleted
inserted
replaced
3 # $Id$ |
3 # $Id$ |
4 # Author: Markus Wenzel, TU Muenchen |
4 # Author: Markus Wenzel, TU Muenchen |
5 # |
5 # |
6 # Isabelle process startup script. |
6 # Isabelle process startup script. |
7 |
7 |
|
8 if [ -L "$0" ]; then |
|
9 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
|
10 exec $(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET") "$@" |
|
11 fi |
|
12 |
8 |
13 |
9 ## settings |
14 ## settings |
10 |
15 |
11 PRG="$(basename "$0")" |
16 PRG="$(basename "$0")" |
12 |
17 |
13 THIS="$0" |
18 ISABELLE_HOME="$(dirname "$0")/.." |
14 while [ -L "$THIS" ]; do |
|
15 THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')" |
|
16 done |
|
17 ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)" |
|
18 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
19 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
19 { echo "$PRG probably not called from its original place!"; exit 2; } |
20 { echo "$PRG probably not called from its original place!"; exit 2; } |
20 |
21 |
21 |
22 |
22 ## diagnostics |
23 ## diagnostics |