# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1702060587 -3600
# Node ID a0e8efbcf18d25161711bf0b30729a15d5467db4
# Parent  d1d6dbab2901d03e4cacc256b603076790c0db18
consider schedule calculation time in estimation;

diff -r d1d6dbab2901 -r a0e8efbcf18d src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Dec 08 18:56:19 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Dec 08 19:36:27 2023 +0100
@@ -980,7 +980,7 @@
         else {
           val start = Time.now()
 
-          val new_schedule = scheduler.build_schedule(state)
+          val new_schedule = scheduler.build_schedule(state).update(state)
           val schedule =
             if (_schedule.graph.is_empty) new_schedule
             else List(_schedule.update(state), new_schedule).minBy(_.end)(Date.Ordering)