changeset 3503 | 390093b95cb0 |
parent 3055 | 5da4afa207ad |
child 4333 | 1d326b826851 |
--- a/lib/scripts/run-polyml Mon Jul 07 09:05:16 1997 +0200 +++ b/lib/scripts/run-polyml Mon Jul 07 09:06:26 1997 +0200 @@ -4,7 +4,7 @@ # # Poly/ML startup script. # -# Global vars: INFILE OUTFILE MLTEXT TERMINATE, +# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE, # and from settings @@ -75,5 +75,6 @@ NEW_DB_INFO=$(ls -l "$DB") [ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE" +[ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" exit $RC