# HG changeset patch
# User wenzelm
# Date 1392067326 -3600
# Node ID 0c15ac6edcf768ff2f6b4d5ca5f2946db486d9ef
# Parent  169e12bbf9a3a163e4fec748d7abfc1a92f41981
make triple-sure that the future scheduler is properly shutdown (see also 702278df3b57);

diff -r 169e12bbf9a3 -r 0c15ac6edcf7 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Feb 10 22:08:18 2014 +0100
+++ b/src/Pure/System/session.ML	Mon Feb 10 22:22:06 2014 +0100
@@ -57,6 +57,7 @@
   Outer_Syntax.check_syntax ();
   Future.shutdown ();
   Event_Timer.shutdown ();
+  Future.shutdown ();
   session_finished := true);