# HG changeset patch
# User wenzelm
# Date 1676142577 -3600
# Node ID 1e2670d9dc18206f37b2faa0bb654230919a36d3
# Parent  2e5a3955bc69776ae9b638b6d8644b7453c26eea
tuned message: old_time not sufficiently prominent nor accurate to be printed;

diff -r 2e5a3955bc69 -r 1e2670d9dc18 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 20:05:30 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 20:09:37 2023 +0100
@@ -53,7 +53,6 @@
   ) {
     def is_empty: Boolean = old_time.is_zero && old_command_timings.isEmpty
 
-    override def toString: String =
-      session + (if (old_time.seconds > 0.0) " (" + old_time.message_hms + " elapsed time)" else "")
+    override def toString: String = session
   }
 }