lib/scripts/run-polyml-5.0
changeset 25124 a7dd8d3bf969
parent 24480 97c0ef49fa8f
child 26213 3a190cb91c6c
equal deleted inserted replaced
25123:8831ca91f43f 25124:a7dd8d3bf969
    65 fi
    65 fi
    66 
    66 
    67 
    67 
    68 ## run it!
    68 ## run it!
    69 
    69 
    70 MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
    70 MLTEXT="$EXIT $COMMIT $MLTEXT"
    71 MLEXIT="commit();"
    71 MLEXIT="commit();"
    72 
    72 
    73 if [ -z "$TERMINATE" ]; then
    73 if [ -z "$TERMINATE" ]; then
    74   FEEDER_OPTS=""
    74   FEEDER_OPTS=""
    75 else
    75 else