# HG changeset patch
# User wenzelm
# Date 1354918479 -3600
# Node ID 702278df3b57aff4c55fec3bffb0206ace927432
# Parent  f8cd5e53653b98df3433356a94bbb3810042c626
make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);

diff -r f8cd5e53653b -r 702278df3b57 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Fri Dec 07 23:11:01 2012 +0100
+++ b/src/Pure/System/session.ML	Fri Dec 07 23:14:39 2012 +0100
@@ -79,6 +79,7 @@
   Keyword.status ();
   Outer_Syntax.check_syntax ();
   Options.reset_default ();
+  Future.shutdown ();
   session_finished := true);