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