--- a/lib/scripts/run-polyml Wed Mar 08 17:39:08 2000 +0100
+++ b/lib/scripts/run-polyml Wed Mar 08 17:40:24 2000 +0100
@@ -4,7 +4,7 @@
#
# Poly/ML startup script.
#
-# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
+# Global vars: INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
# and from settings
@@ -85,7 +85,7 @@
RC=$?
NEW_DB_INFO=$(ls -l "$DB")
-[ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
+[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
exit $RC