| changeset 2344 | c3e1eaea4418 |
| parent 2307 | 508d2a233dbc |
| child 2395 | c24a79fe3651 |
| 2343:2588b63b42ca | 2344:c3e1eaea4418 |
|---|---|
1 #!/bin/bash |
1 #!/bin/bash -norc |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # Isabelle tool starter -- keeps your PATH name space clean. |
5 # Isabelle tool starter -- keeps your PATH name space clean. |
6 |
6 |
37 exit 1 |
37 exit 1 |
38 } |
38 } |
39 |
39 |
40 function fail() |
40 function fail() |
41 { |
41 { |
42 echo "$1" |
42 echo "$1" >&2 |
43 exit 2 |
43 exit 2 |
44 } |
44 } |
45 |
|
46 |
45 |
47 |
46 |
48 ## main |
47 ## main |
49 |
48 |
50 [ $# -lt 1 ] && usage |
49 [ $# -lt 1 ] && usage |