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