equal
deleted
inserted
replaced
12 |
12 |
13 THIS="$0" |
13 THIS="$0" |
14 while [ -L "$THIS" ]; do |
14 while [ -L "$THIS" ]; do |
15 THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')" |
15 THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')" |
16 done |
16 done |
17 ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)" |
17 ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)" |
18 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
18 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
19 { echo "$PRG probably not called from its original place!"; exit 2; } |
19 { echo "$PRG probably not called from its original place!"; exit 2; } |
20 |
20 |
21 |
21 |
22 ## diagnostics |
22 ## diagnostics |