# HG changeset patch
# User wenzelm
# Date 1676121511 -3600
# Node ID dd8f8445b8a4e99c802a7eaf0416e81239fef468
# Parent  2ff94ba221405dcb1d40f41d77c1d850352bc15a
tuned message;

diff -r 2ff94ba22140 -r dd8f8445b8a4 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 14:16:54 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 14:18:31 2023 +0100
@@ -54,6 +54,6 @@
     def is_empty: Boolean = elapsed.is_zero && command_timings.isEmpty
 
     override def toString: String =
-      session + (if (elapsed.is_relevant) " (" + elapsed.message_hms + " elapsed time)" else "")
+      session + (if (elapsed.seconds > 0.0) " (" + elapsed.message_hms + " elapsed time)" else "")
   }
 }