author | wenzelm |
Mon, 14 Nov 2005 15:14:59 +0100 | |
changeset 18166 | b7c3136f604d |
parent 18165 | cbed396ecb1c |
child 18167 | 4f9410e685df |
--- a/lib/scripts/run-polyml Mon Nov 14 15:14:32 2005 +0100 +++ b/lib/scripts/run-polyml Mon Nov 14 15:14:59 2005 +0100 @@ -77,7 +77,7 @@ polyml-4.1.[12]) DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180" ;; - polyml-4.1.*) + polyml-4.1.[34] | polyml-4.2.*) DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" ;; esac @@ -108,7 +108,7 @@ case "$ML_SYSTEM" in polyml-4.1.[12]) ;; - polyml-4.1.*) + polyml-4.1.[34] | polyml-4.2.*) MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $MLTEXT" ;; esac