--- 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