equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
|
3 # $Id$ |
|
4 # |
3 # Isabelle tool starter -- keeps your PATH name space clean. |
5 # Isabelle tool starter -- keeps your PATH name space clean. |
4 # |
|
5 # $Id$ |
|
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 |
12 |
|
13 |
12 |
14 |
13 |
15 ## diagnostics |
14 ## diagnostics |
16 |
15 |
17 PRG=$(basename $0) |
16 PRG=$(basename $0) |