equal
deleted
inserted
replaced
5 # |
5 # |
6 # Isabelle process startup script. |
6 # Isabelle process 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 "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
11 fi |
11 fi |
12 |
12 |
13 |
13 |
14 ## settings |
14 ## settings |
15 |
15 |
16 PRG="$(basename "$0")" |
16 PRG="$(basename "$0")" |
17 |
17 |
18 ISABELLE_HOME="$(dirname "$0")/.." |
18 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
19 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
19 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
20 { echo "$PRG probably not called from its original place!"; exit 2; } |
|
21 |
20 |
22 |
21 |
23 ## diagnostics |
22 ## diagnostics |
24 |
23 |
25 function usage() |
24 function usage() |