# HG changeset patch
# User wenzelm
# Date 868259186 -7200
# Node ID 390093b95cb0c96b477e44abb57b13cc982863bd
# Parent  ec22ba0a26ecb60b8875102267cc222e28e678f6
NOWRITE;

diff -r ec22ba0a26ec -r 390093b95cb0 lib/scripts/run-polyml
--- 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
diff -r ec22ba0a26ec -r 390093b95cb0 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Mon Jul 07 09:05:16 1997 +0200
+++ b/lib/scripts/run-smlnj	Mon Jul 07 09:06:26 1997 +0200
@@ -4,7 +4,7 @@
 #
 # SML/NJ startup script (for 1.06 or later).
 #
-# Global vars: INFILE OUTFILE MLTEXT TERMINATE,
+# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
 # and from settings
 
 
@@ -74,4 +74,6 @@
 [ -n "$OUTFILE" -a -n "$SUFFIX" -a -f "$OUTFILE$SUFFIX" ] \
   && mv "$OUTFILE$SUFFIX" "$OUTFILE"
 
+[ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
 exit $RC
diff -r ec22ba0a26ec -r 390093b95cb0 lib/scripts/run-smlnj-0.93
--- a/lib/scripts/run-smlnj-0.93	Mon Jul 07 09:05:16 1997 +0200
+++ b/lib/scripts/run-smlnj-0.93	Mon Jul 07 09:06:26 1997 +0200
@@ -4,7 +4,7 @@
 #
 # SML/NJ startup script (for 0.93).
 #
-# Global vars: INFILE OUTFILE MLTEXT TERMINATE,
+# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
 # and from settings
 
 
@@ -60,6 +60,8 @@
   RC=$?
 fi
 
+[ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
 if [ -n "$MOVE" -a -f "$OUTFILE" ]; then
   rm -f "$INFILE" || fail_out
   mv "$OUTFILE" "$INFILE" || fail_out