author | Fabian Huch <huch@in.tum.de> |
Fri, 08 Dec 2023 19:36:27 +0100 | |
changeset 79194 | a0e8efbcf18d |
parent 79193 | d1d6dbab2901 |
child 79218 | 8857975b99a9 |
--- 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)