equal
deleted
inserted
replaced
10 |
10 |
11 PRG=$(basename $0) |
11 PRG=$(basename $0) |
12 |
12 |
13 ISABELLE_HOME=$(dirname $0)/.. |
13 ISABELLE_HOME=$(dirname $0)/.. |
14 . $ISABELLE_HOME/lib/scripts/getsettings || \ |
14 . $ISABELLE_HOME/lib/scripts/getsettings || \ |
15 { echo "$PRG probably not called from its original place!"; exit 2 } |
15 { echo "$PRG probably not called from its original place!"; exit 2; } |
16 |
16 |
17 |
17 |
18 ## diagnostics |
18 ## diagnostics |
19 |
19 |
20 TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ") |
20 TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ") |