equal
deleted
inserted
replaced
7 |
7 |
8 ## settings |
8 ## settings |
9 |
9 |
10 PRG=$(basename $0) |
10 PRG=$(basename $0) |
11 |
11 |
12 ISABELLE_HOME=$(dirname $(dirname $0)) |
12 ISABELLE_HOME=$(dirname $0)/.. |
13 case "$ISABELLE_HOME" in |
13 . $ISABELLE_HOME/lib/scripts/getsettings || \ |
14 /*) |
14 { echo "$PRG probably not called from its original place!"; exit 2 } |
15 if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then |
|
16 . $ISABELLE_HOME/lib/scripts/getsettings || exit 2 |
|
17 else |
|
18 echo "ERROR: $PRG probably not called from its original place!" |
|
19 exit 1 |
|
20 fi |
|
21 ;; |
|
22 *) |
|
23 echo "ERROR: $PRG not called with absolute path specification!" |
|
24 exit 1 |
|
25 ;; |
|
26 esac |
|
27 |
15 |
28 |
16 |
29 ## diagnostics |
17 ## diagnostics |
30 |
18 |
31 function usage() |
19 function usage() |