# HG changeset patch
# User wenzelm
# Date 1350504672 -7200
# Node ID 03871053cdba78bd89d2546ffa9ba51d2385c64a
# Parent  69bfd86cc711da79e8c5e98e35ab7be153eba325
another Future.shutdown after Future.cancel_groups (cf. 0d4106850eb2);

diff -r 69bfd86cc711 -r 03871053cdba src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Wed Oct 17 21:18:32 2012 +0200
+++ b/src/Pure/System/session.ML	Wed Oct 17 22:11:12 2012 +0200
@@ -74,6 +74,7 @@
     Future.shutdown ();
     Goal.finish_futures ();
     Goal.cancel_futures ();
+    Future.shutdown ();
     Options.reset_default ();
     session_finished := true);