author | wenzelm |
Mon, 08 Apr 2013 15:44:09 +0200 | |
changeset 52774 | ff2d241dcde1 |
parent 52773 | e49bf0be79ba |
child 52775 | 1275716f395b |
1.1 --- a/src/Pure/Concurrent/future.ML Mon Apr 08 15:35:48 2013 +0200 1.2 +++ b/src/Pure/Concurrent/future.ML Mon Apr 08 15:44:09 2013 +0200 1.3 @@ -341,7 +341,6 @@ 1.4 1.5 val mm = 1.6 if ! do_shutdown then 0 1.7 - else if m = 9999 then 1 1.8 else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 4 * m); 1.9 val _ = 1.10 if tick andalso mm > ! max_workers then