# HG changeset patch # User wenzelm # Date 1420922389 -3600 # Node ID b02b1fbcf05118aea768235592ea26a64b3d1fd1 # Parent e0ce214303c120aeea9265a013af6922a1741802 tuned -- less redundant; diff -r e0ce214303c1 -r b02b1fbcf051 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Sat Jan 10 21:22:25 2015 +0100 +++ b/src/Pure/PIDE/session.ML Sat Jan 10 21:39:49 2015 +0100 @@ -72,7 +72,6 @@ fun save heap = (Execution.shutdown (); - Future.shutdown (); Event_Timer.shutdown (); Future.shutdown (); ML_System.share_common_data ();