# HG changeset patch
# User wenzelm
# Date 952533624 -3600
# Node ID 885a6414b9c8d3f51729ec800446014c2e2e269b
# Parent  124ad46105dd30ba77157e7fc2c70def83e5e1da
observe COMPRESS option;

diff -r 124ad46105dd -r 885a6414b9c8 lib/scripts/run-polyml
--- 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