--- a/src/Pure/Build/build_schedule.scala Thu Mar 14 17:19:01 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Thu Mar 14 17:27:40 2024 +0100
@@ -502,7 +502,7 @@
def end: Date =
if (graph.is_empty) start
- else graph.maximals.map(graph.get_node).map(_.end).maxBy(_.unix_epoch)
+ else graph.maximals.map(graph.get_node).map(_.end).max(Date.Ordering)
def duration: Time = end - start
def message: String = "Estimated " + duration.message_hms + " build time with " + generator
@@ -536,7 +536,7 @@
def shift_elapsed(graph: Schedule.Graph, name: String): Schedule.Graph =
graph.map_node(name, { node =>
val elapsed = start1 - state.running(name).start_date
- node.copy(duration = node.duration - elapsed)
+ node.copy(duration = (node.duration - elapsed).max(Time.zero))
})
def shift_starts(graph: Schedule.Graph, name: String): Schedule.Graph =