tuned message;
authorFabian Huch <huch@in.tum.de>
Mon, 13 Nov 2023 18:08:05 +0100
changeset 78976 8da0eedd562c
parent 78975 4a5d35b35aeb
child 78977 c7db5b4dbace
tuned message;
src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Mon Nov 13 17:48:11 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Mon Nov 13 18:08:05 2023 +0100
@@ -628,7 +628,7 @@
           val estimate = Date(Time.now() + scheduler.build_duration(state))
           val elapsed = Time.now() - start
 
-          val timing_msg = if (elapsed.is_relevant) " (in " + elapsed.message + ")" else ""
+          val timing_msg = if (elapsed.is_relevant) " (took " + elapsed.message + ")" else ""
           progress.echo_if(build_context.master && !cache.is_current_estimate(estimate),
             "Estimated completion: " + estimate + timing_msg)