| changeset 2395 | c24a79fe3651 |
| parent 2344 | c3e1eaea4418 |
| child 2434 | d3d42a2e7da2 |
| 2394:91d8abf108be | 2395:c24a79fe3651 |
|---|---|
6 |
6 |
7 |
7 |
8 ## settings |
8 ## settings |
9 |
9 |
10 ISABELLE_HOME=$(dirname $(dirname $0)) |
10 ISABELLE_HOME=$(dirname $(dirname $0)) |
11 . $ISABELLE_HOME/lib/scripts/getsettings |
11 . $ISABELLE_HOME/lib/scripts/getsettings || exit 2 |
12 |
12 |
13 |
13 |
14 ## diagnostics |
14 ## diagnostics |
15 |
15 |
16 PRG=$(basename $0) |
16 PRG=$(basename $0) |