equal
deleted
inserted
replaced
8 |
8 |
9 ## settings |
9 ## settings |
10 |
10 |
11 PRG="$(basename "$0")" |
11 PRG="$(basename "$0")" |
12 |
12 |
13 ISABELLE_HOME="$(dirname "$0")/.." |
13 THIS="$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 "$(readlink -f "$THIS")")/.."; pwd)" |
14 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
18 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
15 { echo "$PRG probably not called from its original place!"; exit 2; } |
19 { echo "$PRG probably not called from its original place!"; exit 2; } |
16 |
20 |
17 |
21 |
18 ## diagnostics |
22 ## diagnostics |