| changeset 51637 | ff2d241dcde1 |
| parent 51354 | 45579fbe5a24 |
| child 51661 | 92e58b76dbb1 |
--- 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