lib/scripts/run-mosml
changeset 10105 f9be78009930
parent 9997 38598a19e701
child 10555 2323ec838401
equal deleted inserted replaced
10104:cf49932f3c42 10105:f9be78009930
     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
     9 export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
    10 
    10 
    11 
    11 
    12 ## diagnostics
    12 ## diagnostics
    13 
    13 
    14 function fail_out()
    14 function fail_out()