lib/scripts/run-polyml
changeset 8360 885a6414b9c8
parent 5063 d45ec8d00ab0
child 8821 b5c3aec69462
--- 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