equal
deleted
inserted
replaced
5 # Isabelle tool starter -- keeps your PATH name space clean. |
5 # Isabelle tool starter -- keeps your PATH name space clean. |
6 |
6 |
7 |
7 |
8 ## settings |
8 ## settings |
9 |
9 |
|
10 PRG=$(basename $0) |
|
11 |
10 ISABELLE_HOME=$(dirname $(dirname $0)) |
12 ISABELLE_HOME=$(dirname $(dirname $0)) |
11 . $ISABELLE_HOME/lib/scripts/getsettings || exit 2 |
13 case "$ISABELLE_HOME" in |
|
14 /*) |
|
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 |
12 |
27 |
13 |
28 |
14 ## diagnostics |
29 ## diagnostics |
15 |
|
16 PRG=$(basename $0) |
|
17 |
30 |
18 function usage() |
31 function usage() |
19 { |
32 { |
20 echo |
33 echo |
21 echo "Usage: $PRG TOOL [ARGS ...]" |
34 echo "Usage: $PRG TOOL [ARGS ...]" |