src/Pure/Tools/build.scala
changeset 62486 b737f8f37454
parent 62477 bc6e771e98a6
child 62490 39d01eaf5292
     1.1 --- a/src/Pure/Tools/build.scala	Tue Mar 01 14:47:27 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 01 15:48:19 2016 +0100
     1.3 @@ -589,7 +589,7 @@
     1.4              "$ISABELLE_PROCESS" \
     1.5                -e 'use """ + quote(ml_root) + """ handle _ => OS.Process.exit OS.Process.failure;' \
     1.6                -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
     1.7 -              -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
     1.8 +              -q RAW_ML_SYSTEM
     1.9            """
    1.10          }
    1.11          else {
    1.12 @@ -598,15 +598,10 @@
    1.13              "$ISABELLE_PROCESS" \
    1.14                -e '(use """ + quote(ml_root) + """; use "ROOT.ML") handle _ => OS.Process.exit OS.Process.failure;' \
    1.15                -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
    1.16 -              -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
    1.17 +              -q RAW_ML_SYSTEM
    1.18            """
    1.19          }
    1.20        }
    1.21 -      else if (do_output)
    1.22 -        """
    1.23 -        rm -f "$OUTPUT"
    1.24 -        "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q "$INPUT" && chmod -w "$OUTPUT"
    1.25 -        """
    1.26        else
    1.27          """
    1.28          rm -f "$OUTPUT"