diff -r d97e13e5ea5b -r 6d292ee30365 src/Pure/build --- a/src/Pure/build Mon Feb 29 15:39:17 2016 +0100 +++ b/src/Pure/build Mon Feb 29 16:12:47 2016 +0100 @@ -64,11 +64,13 @@ -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ -q RAW_ML_SYSTEM else + rm -f "$OUTPUT" "$ISABELLE_PROCESS" \ -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ -e "structure Isar = struct fun main () = () end;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ - -q -w RAW_ML_SYSTEM "$OUTPUT" + -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ + -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" fi else if [ -z "$OUTPUT" ]; then @@ -76,12 +78,15 @@ -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ -q RAW_ML_SYSTEM else + rm -f "$OUTPUT" "$ISABELLE_PROCESS" \ -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ -e "Command_Line.tool0 Session.finish;" \ -e "Options.reset_default ();" \ - -q -w RAW_ML_SYSTEM "$OUTPUT" + -e "Session.shutdown ();" \ + -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ + -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" fi fi