# HG changeset patch
# User wenzelm
# Date 1677494585 -3600
# Node ID cb92bd1c6f8c37c201d460423e72167736b4fe89
# Parent  467a8f987b5a6d75afaf376dc7def31357228e4d
clarified signature;

diff -r 467a8f987b5a -r cb92bd1c6f8c src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Feb 27 11:19:16 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 27 11:43:05 2023 +0100
@@ -489,8 +489,8 @@
 
   /* main process */
 
-  def session_finished(session_name: String, process_result: Process_Result): String =
-    "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
+  def session_finished(session_name: String, timing: Timing): String =
+    "Finished " + session_name + " (" + timing.message_resources + ")"
 
   def session_timing(session_name: String, build_log: Build_Log.Session_Info): String = {
     val props = build_log.session_timing
@@ -586,7 +586,7 @@
 
     if (process_result.ok) {
       if (verbose) progress.echo(Build_Process.session_timing(session_name, build_log))
-      progress.echo(Build_Process.session_finished(session_name, process_result))
+      progress.echo(Build_Process.session_finished(session_name, process_result.timing))
     }
     else {
       progress.echo(