1.1 --- a/lib/scripts/run-polyml	Mon Nov 14 15:14:32 2005 +0100
     1.2 +++ b/lib/scripts/run-polyml	Mon Nov 14 15:14:59 2005 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4      polyml-4.1.[12])
     1.5        DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
     1.6        ;;
     1.7 -    polyml-4.1.*)
     1.8 +    polyml-4.1.[34] | polyml-4.2.*)
     1.9        DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
    1.10        ;;
    1.11    esac
    1.12 @@ -108,7 +108,7 @@
    1.13  case "$ML_SYSTEM" in
    1.14    polyml-4.1.[12])
    1.15      ;;
    1.16 -  polyml-4.1.*)
    1.17 +  polyml-4.1.[34] | polyml-4.2.*)
    1.18      MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $MLTEXT"
    1.19      ;;
    1.20  esac