# HG changeset patch
# User wenzelm
# Date 1699002821 -3600
# Node ID b82c2f801f2c5de21b2819bc3291c98dd3db5197
# Parent  0233d5a5a4caf0ea7af6c67b7228c459b0e0aabd# Parent  9d0faaa77e5d04ea3fde7669406d9b3eeefcbdac
merged

diff -r 9d0faaa77e5d -r b82c2f801f2c src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Nov 03 10:12:34 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 03 10:13:41 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)