tuned whitespace;
authorwenzelm
Thu, 02 Nov 2023 14:31:01 +0100
changeset 78880 9ce8bf038444
parent 78879 2e260496a4f8
child 78882 c1bd24ca22b6
tuned whitespace;
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))) {