| changeset 2936 | bd33e7aae062 |
| parent 2918 | 0305b0acba78 |
| child 3007 | e5efa177ee0c |
| 2935:998cb95fdd43 | 2936:bd33e7aae062 |
|---|---|
9 |
9 |
10 PRG=$(basename $0) |
10 PRG=$(basename $0) |
11 |
11 |
12 ISABELLE_HOME=$(dirname $0) |
12 ISABELLE_HOME=$(dirname $0) |
13 . $ISABELLE_HOME/lib/scripts/getsettings || \ |
13 . $ISABELLE_HOME/lib/scripts/getsettings || \ |
14 { echo "$PRG probably not called from its original place!"; exit 2 } |
14 { echo "$PRG probably not called from its original place!"; exit 2; } |
15 |
15 |
16 |
16 |
17 ## diagnostics |
17 ## diagnostics |
18 |
18 |
19 function usage() |
19 function usage() |