diff -r 8bcecefd2e89 -r 75954ae8b247 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Sun Jun 05 17:46:06 2005 +0200
+++ b/lib/scripts/run-polyml	Sun Jun 05 21:32:37 2005 +0200
@@ -49,14 +49,6 @@
 
     DISCGARB="$POLY"
     DISCGARB_OPTIONS="-d -c"
-    case "$ML_SYSTEM" in
-      polyml-4.1.[12])
-	DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
-	;;
-      polyml-4.1.*)
-	DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
-	;;
-    esac
 
     EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
     ;;
@@ -80,6 +72,14 @@
   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.*)
+      DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
+      ;;
+  esac
 else
   COPYDB=true
 fi