equal
deleted
inserted
replaced
3 # $Id$ |
3 # $Id$ |
4 # Author: Markus Wenzel, TU Muenchen |
4 # Author: Markus Wenzel, TU Muenchen |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
6 # |
6 # |
7 # Moscow ML 2.00 startup script |
7 # Moscow ML 2.00 startup script |
8 # |
8 |
9 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP, |
9 export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP |
10 # and from settings |
|
11 |
10 |
12 |
11 |
13 ## diagnostics |
12 ## diagnostics |
14 |
13 |
15 function fail_out() |
14 function fail_out() |