src/Pure/Concurrent/future.ML
changeset 40301 bf39a257b3d3
parent 39243 307e3d07d19f
child 40448 f9347a30d1b2
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Nov 02 20:31:46 2010 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Nov 02 20:55:12 2010 +0100
     1.3 @@ -253,7 +253,7 @@
     1.4  val status_ticks = Unsynchronized.ref 0;
     1.5  
     1.6  val last_round = Unsynchronized.ref Time.zeroTime;
     1.7 -val next_round = Time.fromMilliseconds 50;
     1.8 +val next_round = seconds 0.05;
     1.9  
    1.10  fun scheduler_next () = (*requires SYNCHRONIZED*)
    1.11    let