diff -r a1297de19ec7 -r b5c3aec69462 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Sat May 06 00:46:13 2000 +0200
+++ b/lib/scripts/run-polyml	Mon May 08 10:49:27 2000 +0200
@@ -34,12 +34,6 @@
 check_mlhome_file "$POLY"
 check_mlhome_file "$DISCGARB"
 
-case "$ML_SYSTEM" in
-  polyml-3.*)
-    DISCGARB="$DISCGARB -c"
-    ;;
-esac
-
 
 ## prepare databases
 
@@ -85,7 +79,7 @@
 RC=$?
 
 NEW_DB_INFO=$(ls -l "$DB")
-[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
+[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB -c "$OUTFILE"
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
 exit $RC