discontinued odd magic number, which was once used for performance measurements;
authorwenzelm
Mon, 08 Apr 2013 15:44:09 +0200
changeset 52774ff2d241dcde1
parent 52773 e49bf0be79ba
child 52775 1275716f395b
discontinued odd magic number, which was once used for performance measurements;
src/Pure/Concurrent/future.ML
     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