# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719565744 -7200
# Node ID 9f90c4864e55ade9b4cb646d3935ce44256e9000
# Parent  10ab5a74f6f5088962b63b56702d648d7a694bd8
add timing messages;

diff -r 10ab5a74f6f5 -r 9f90c4864e55 src/Pure/Build/build_ci.scala
--- a/src/Pure/Build/build_ci.scala	Fri Jun 28 10:58:29 2024 +0200
+++ b/src/Pure/Build/build_ci.scala	Fri Jun 28 11:09:04 2024 +0200
@@ -189,6 +189,16 @@
         max_jobs = job.hosts.max_jobs)
     }
 
+    val stop_date = progress.now()
+    val elapsed_time = stop_date - progress.start
+    progress.echo("\nFinished at " + Build_Log.print_date(stop_date))
+
+    progress.echo(section("TIMING"))
+    val total_timing =
+      results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
+        copy(elapsed = elapsed_time)
+    progress.echo(total_timing.message_resources)
+
     val post_result = return_code { job.hook.post(options, url, results, progress) }
 
     val rc = List(mail_result, pre_result, results.rc, post_result).max