# HG changeset patch
# User wenzelm
# Date 1361879452 -3600
# Node ID 12b7b0baaa1eb4842d7483bc8a669a6925b9c57b
# Parent  f4a2fa9286e970b2f411e5782761ccdb009dcc0f
less eventful shutdown: merely wait for scheduler to terminate;

diff -r f4a2fa9286e9 -r 12b7b0baaa1e src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Feb 26 12:46:47 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 26 12:50:52 2013 +0100
@@ -686,8 +686,7 @@
     SYNCHRONIZED "shutdown" (fn () =>
       while scheduler_active () do
        (Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
-        wait scheduler_event;
-        broadcast_work ()))
+        wait scheduler_event))
   else ();