author | wenzelm |
Sat, 11 Feb 2023 14:18:31 +0100 | |
changeset 77241 | dd8f8445b8a4 |
parent 77240 | 2ff94ba22140 |
child 77242 | 7c89e848bd18 |
--- 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 "") } }