# HG changeset patch
# User wenzelm
# Date 1677847854 -3600
# Node ID c546e3e1f7f6f1fcceadf41aa0fbfdbec8156f9f
# Parent  1a32b4928aad79dec0b7f973c85381ebc2da1450
tuned signature;

diff -r 1a32b4928aad -r c546e3e1f7f6 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Mar 03 13:50:39 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Fri Mar 03 13:50:54 2023 +0100
@@ -359,15 +359,17 @@
             val rc = res.int(Results.rc)
             val out = res.string(Results.out)
             val err = res.string(Results.err)
-            val timing_elapsed = res.long(Results.timing_elapsed)
-            val timing_cpu = res.long(Results.timing_cpu)
-            val timing_gc = res.long(Results.timing_gc)
+            val timing =
+              res.timing(
+                Results.timing_elapsed,
+                Results.timing_cpu,
+                Results.timing_gc)
             val node_info = Host.Node_Info(hostname, numa_node)
             val process_result =
               Process_Result(rc,
                 out_lines = split_lines(out),
                 err_lines = split_lines(err),
-                timing = Timing(Time.ms(timing_elapsed), Time.ms(timing_cpu), Time.ms(timing_gc)))
+                timing = timing)
             name -> Build_Job.Result(node_info, process_result)
           })
       }