redundant -- already part of Session.finish;
authorwenzelm
Mon, 29 Feb 2016 16:25:51 +0100
changeset 62471 e3f3854f460e
parent 62470 9037ed690e19
child 62472 01e2bd5b4027
redundant -- already part of Session.finish;
src/Pure/Tools/build.ML
--- 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);