# HG changeset patch
# User wenzelm
# Date 1192905110 -7200
# Node ID 8831ca91f43f5e64311493ff35686c095a8ef23f
# Parent  f37d7dd25c8856306cb6471398acd2ae58378b04
discontinued support for 4.1.1, 4.1.2;

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