diff -r f37d7dd25c88 -r 8831ca91f43f lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Sat Oct 20 18:54:35 2007 +0200
+++ b/lib/scripts/run-polyml	Sat Oct 20 20:31:50 2007 +0200
@@ -61,14 +61,7 @@
   check_file "$ML_DBASE_PREFIX$ML_DBASE"
   INFILE="$ML_DBASE"
   MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
-  case "$ML_SYSTEM" in
-    polyml-4.1.[12])
-      DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
-      ;;
-    polyml-4.1.[34] | polyml-4.2.*)
-      DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
-      ;;
-  esac
+  DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
 else
   COPYDB=true
 fi
@@ -93,14 +86,6 @@
 
 ## run it!
 
-case "$ML_SYSTEM" in
-  polyml-4.1.[12])
-    ;;
-  polyml-4.1.[34] | polyml-4.2.*)
-    MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $MLTEXT"
-    ;;
-esac
-
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""
 else