# HG changeset patch
# User wenzelm
# Date 1365428649 -7200
# Node ID ff2d241dcde13df4f5ee5694102f99fdcbb3d19b
# Parent  e49bf0be79ba61869f2858ae4830f23527b42b34
discontinued odd magic number, which was once used for performance measurements;

diff -r e49bf0be79ba -r ff2d241dcde1 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Apr 08 15:35:48 2013 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Apr 08 15:44:09 2013 +0200
@@ -341,7 +341,6 @@
 
     val mm =
       if ! do_shutdown then 0
-      else if m = 9999 then 1
       else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 4 * m);
     val _ =
       if tick andalso mm > ! max_workers then