# HG changeset patch # User Fabian Huch # 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 {