add timing messages;
authorFabian Huch <huch@in.tum.de>
Fri, 28 Jun 2024 11:09:04 +0200
changeset 80418 9f90c4864e55
parent 80417 10ab5a74f6f5
child 80419 788b6af566ff
add timing messages;
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