# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701349701 -3600
# Node ID 59d5d1e2639380ff816550b3d5140ed8a0027950
# Parent  cf51ccfd3e39a1f4d3da098306e4812a4ed2f3a1
lower bound for approximated times;

diff -r cf51ccfd3e39 -r 59d5d1e26393 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 30 14:02:52 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 30 14:08:21 2023 +0100
@@ -84,7 +84,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 = t_c + t_p.scale(1.0 / threads)
+        def model(threads: Int): Time = Time.ms((t_c + t_p.scale(1.0 / threads)).ms max 0)
 
         if (is_mono || in_prefix) model(threads)
         else {