removed obsolete chmod: isabelle_process no longer supports writable heaps;
authorwenzelm
Tue, 01 Mar 2016 15:48:19 +0100
changeset 62486 b737f8f37454
parent 62485 a04e26352106
child 62487 fc353b09325d
removed obsolete chmod: isabelle_process no longer supports writable heaps;
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"