author | wenzelm |
Mon, 29 Feb 2016 16:25:51 +0100 | |
changeset 62471 | e3f3854f460e |
parent 62470 | 9037ed690e19 |
child 62472 | 01e2bd5b4027 |
--- a/src/Pure/Tools/build.ML Mon Feb 29 16:24:20 2016 +0100 +++ b/src/Pure/Tools/build.ML Mon Feb 29 16:25:51 2016 +0100 @@ -166,7 +166,6 @@ val _ = Par_Exn.release_all [res1, res2]; val _ = Options.reset_default (); - val _ = Session.shutdown (); val _ = if do_output then (ML_Heap.share_common_data (); ML_Heap.save_state output) else (); in () end);