equal
deleted
inserted
replaced
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 # MLWorks startup script (for 1.0r2 or later). |
7 # MLWorks startup script (for 1.0r2 or later). |
8 |
8 |
9 export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP |
9 export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE |
10 |
10 |
11 |
11 |
12 ## diagnostics |
12 ## diagnostics |
13 |
13 |
14 function fail_out() |
14 function fail_out() |