# HG changeset patch
# User wenzelm
# Date 1698931861 -3600
# Node ID 9ce8bf038444c5660fe8f28be194d948311723f0
# Parent  2e260496a4f892aa1e04720a05268db7d67a3735
tuned whitespace;

diff -r 2e260496a4f8 -r 9ce8bf038444 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Nov 02 13:16:06 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Thu Nov 02 14:31:01 2023 +0100
@@ -1070,6 +1070,7 @@
 
       val consumer =
         Consumer_Thread.fork[Log_File]("build_log_database")(
+          limit = 1,
           consume = { log_file =>
             val t0 = progress.start.time
             val t1 = progress.now().time
@@ -1081,16 +1082,13 @@
 
             val t2 = progress.now().time
 
-            progress.echo(verbose = true,
-              msg =
-                "Log " + quote(log_file.name) + " (" +
-                  (t1 - t0).message_hms + " start time, " +
-                  (t2 - t1).message + " elapsed time)")
+            progress.echo(verbose = true, msg =
+              "Log " + quote(log_file.name) + " (" +
+                (t1 - t0).message_hms + " start time, " +
+                (t2 - t1).message + " elapsed time)")
 
             true
-          },
-          limit = 1
-        )
+          })
 
       try {
         for (file <- files.iterator if status.exists(_.required(file))) {