clarified signature;
authorwenzelm
Mon, 27 Feb 2023 11:43:05 +0100
changeset 77393 cb92bd1c6f8c
parent 77392 467a8f987b5a
child 77394 b9214b89d994
clarified signature;
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(