# 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