src/Pure/Tools/build_process.scala
changeset 77245 1e2670d9dc18
parent 77244 2e5a3955bc69
child 77246 173c2fb78290
--- 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
   }
 }