# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701894240 -3600
# Node ID b5b5930bd40a103d270fedf6b86ef48ad1dc5933
# Parent  32d00ec387f4fe5ae2e535edb21498c02014e955
tuned;

diff -r 32d00ec387f4 -r b5b5930bd40a src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Wed Dec 06 20:04:47 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Wed Dec 06 21:24:00 2023 +0100
@@ -63,7 +63,7 @@
       def linear(p0: (Int, Time), p1: (Int, Time)): Time = {
         val a = (p1._2 - p0._2).scale(1.0 / (p1._1 - p0._1))
         val b = p0._2 - a.scale(p0._1)
-        Time.ms((a.scale(threads) + b).ms max 0)
+        (a.scale(threads) + b) max Time.zero
       }
 
       val mono_prefix = sorted_prefix(entries, e => -e._2.ms)
@@ -83,7 +83,7 @@
         val t_c =
           Timing_Data.median_time(for ((n, t) <- mono_prefix) yield t - t_p.scale(1.0 / n))
 
-        def model(threads: Int): Time = Time.ms((t_c + t_p.scale(1.0 / threads)).ms max 0)
+        def model(threads: Int): Time = (t_c + t_p.scale(1.0 / threads)) max Time.zero
 
         if (is_mono || in_prefix) model(threads)
         else {
@@ -694,7 +694,7 @@
             val estimate =
               timing_data.estimate(job.name, job.node_info.hostname,
                 host_infos.num_threads(job.node_info))
-            node -> Time.ms((Time.now() - job.start_date.time + estimate).ms max 0)
+            node -> ((Time.now() - job.start_date.time + estimate) max Time.zero)
         }
 
       val max_parallel = parallel_paths(state.ready.map(_.name).map(remaining_time))