# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710433660 -3600
# Node ID 661fb7db57ca2228f294a446a222a6684b391248
# Parent  2c9c5ae99a09aa21ffbe051c950f3af17ce8cf7f
tuned;

diff -r 2c9c5ae99a09 -r 661fb7db57ca src/Pure/Build/build_schedule.scala
--- 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 =