# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699002185 -3600
# Node ID 0233d5a5a4caf0ea7af6c67b7228c459b0e0aabd
# Parent  5de1c19ccd92aa0b2c2823eea82e0c1dd8cd6b6b
improved build messages;

diff -r 5de1c19ccd92 -r 0233d5a5a4ca src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 02 21:35:04 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 03 10:03:05 2023 +0100
@@ -525,10 +525,14 @@
     override def next_jobs(state: Build_Process.State): List[String] =
       if (cache.is_current(state)) cache.configs.map(_.job_name)
       else {
+        val start = Time.now()
         val next = scheduler.next(timing_data, state)
         val estimate = Date(Time.now() + scheduler.build_duration(timing_data, state))
-        progress.echo_if(build_context.master && cache.is_current_estimate(estimate),
-          "Estimated completion: " + estimate)
+        val elapsed = Time.now() - start
+
+        val timing_msg = if (elapsed.is_relevant) " (in " + elapsed.message + ")" else ""
+        progress.echo_if(build_context.master && !cache.is_current_estimate(estimate),
+          "Estimated completion: " + estimate + timing_msg)
 
         val configs = next.filter(_.node_info.hostname == hostname)
         cache = Cache(state, configs, estimate)