# 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);