# HG changeset patch
# User wenzelm
# Date 1677847839 -3600
# Node ID 1a32b4928aad79dec0b7f973c85381ebc2da1450
# Parent  2d5529f561243cc7b03084d616c0b7ab5089ba53
tuned whitespace;

diff -r 2d5529f56124 -r 1a32b4928aad src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Mar 03 13:39:46 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Fri Mar 03 13:50:39 2023 +0100
@@ -1092,9 +1092,16 @@
                 chapter = res.string(Data.chapter),
                 groups = split_lines(res.string(Data.groups)),
                 threads = res.get_int(Data.threads),
-                timing = res.timing(Data.timing_elapsed, Data.timing_cpu, Data.timing_gc),
+                timing =
+                  res.timing(
+                    Data.timing_elapsed,
+                    Data.timing_cpu,
+                    Data.timing_gc),
                 ml_timing =
-                  res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc),
+                  res.timing(
+                    Data.ml_timing_elapsed,
+                    Data.ml_timing_cpu,
+                    Data.ml_timing_gc),
                 sources = res.get_string(Data.sources),
                 heap_size = res.get_long(Data.heap_size).map(Space.bytes),
                 status = res.get_string(Data.status).map(Session_Status.withName),