# HG changeset patch
# User wenzelm
# Date 1676121414 -3600
# Node ID 2ff94ba221405dcb1d40f41d77c1d850352bc15a
# Parent  b9bf4c0bd47d4df6021d49ef00791739f2999fc9
tuned signature: more operations;

diff -r b9bf4c0bd47d -r 2ff94ba22140 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 12:09:42 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 14:16:54 2023 +0100
@@ -51,6 +51,8 @@
     val elapsed: Time,
     val command_timings: List[Properties.T]
   ) {
+    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 "")
   }