# HG changeset patch
# User wenzelm
# Date 1456843699 -3600
# Node ID b737f8f374548252bb8ff4972336185eb5da6f0e
# Parent  a04e2635210697d93c6ec090b407236e4bb351bd
removed obsolete chmod: isabelle_process no longer supports writable heaps;

diff -r a04e26352106 -r b737f8f37454 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 01 14:47:27 2016 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 01 15:48:19 2016 +0100
@@ -589,7 +589,7 @@
             "$ISABELLE_PROCESS" \
               -e 'use """ + quote(ml_root) + """ handle _ => OS.Process.exit OS.Process.failure;' \
               -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
-              -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
+              -q RAW_ML_SYSTEM
           """
         }
         else {
@@ -598,15 +598,10 @@
             "$ISABELLE_PROCESS" \
               -e '(use """ + quote(ml_root) + """; use "ROOT.ML") handle _ => OS.Process.exit OS.Process.failure;' \
               -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
-              -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
+              -q RAW_ML_SYSTEM
           """
         }
       }
-      else if (do_output)
-        """
-        rm -f "$OUTPUT"
-        "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" && chmod -w "$OUTPUT"
-        """
       else
         """
         rm -f "$OUTPUT"