| changeset 2344 | c3e1eaea4418 |
| parent 2315 | 491e8d4b8fad |
| child 2430 | 7dc83c3d751a |
| 2343:2588b63b42ca | 2344:c3e1eaea4418 |
|---|---|
1 #!/bin/bash |
1 #!/bin/bash -norc |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # Isabelle within an xterm. |
5 # Isabelle within an xterm. |
6 |
6 |
7 |
7 |
8 ## diagnostics |
8 ## diagnostics |
9 |
9 |
10 function fail() |
10 function fail() |
11 { |
11 { |
12 echo "$1" |
12 echo "$1" >&2 |
13 exit 2 |
13 exit 2 |
14 } |
14 } |
15 |
15 |
16 |
16 |
17 ## main |
17 ## main |