lib/scripts/run-mosml
changeset 9997 38598a19e701
parent 9977 32955afeb835
child 10105 f9be78009930
equal deleted inserted replaced
9996:dede9cf1bd2a 9997:38598a19e701
     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 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()