diff -r 389e660549d0 -r e69ebc4782a3 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Tue Sep 16 13:46:43 2025 +0200
+++ b/src/Pure/General/timing.scala	Tue Sep 16 13:52:24 2025 +0200
@@ -36,6 +36,9 @@
 
   def factor_format(f: Double): String =
     String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
+
+  def merge(args: IterableOnce[Timing]): Timing =
+    args.iterator.foldLeft(zero)(_ + _)
 }
 
 sealed case class Timing(elapsed: Time, cpu: Time, gc: Time) {