lib/scripts/run-polyml-5.0
changeset 26213 3a190cb91c6c
parent 25124 a7dd8d3bf969
child 26375 234f10289d97
equal deleted inserted replaced
26212:225b40bf36a7 26213:3a190cb91c6c
     1 #!/usr/bin/env bash
     1 #!/usr/bin/env bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 # Author: Makarius
     4 # Author: Makarius
     5 #
     5 #
     6 # Poly/ML startup script (for 5.0)
     6 # Poly/ML 5.0 startup script.
     7 
     7 
     8 export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
     8 export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
     9 
     9 
    10 
    10 
    11 ## diagnostics
    11 ## diagnostics