# HG changeset patch
# User wenzelm
# Date 1456759551 -3600
# Node ID e3f3854f460efe9ef9a2bd7125de0ab52ce651e7
# Parent  9037ed690e19f6250776bf639fb8615a6afe2b56
redundant -- already part of Session.finish;

diff -r 9037ed690e19 -r e3f3854f460e 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);