tuned;
authorwenzelm
Mon, 06 Mar 2023 10:08:53 +0100
changeset 77533 8f464df3520a
parent 77532 69af424b1f9d
child 77534 fc57886e37dd
tuned;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 06 09:50:48 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 06 10:08:53 2023 +0100
@@ -680,14 +680,14 @@
 
   /* progress backed by database */
 
-  private def progress_output(message: Progress.Message, body: => Unit): Unit = {
+  private def progress_output(message: Progress.Message, build_progress_output: => Unit): Unit = {
     synchronized_database {
       val state1 = _state.inc_serial.progress_serial()
       for (db <- _database) {
         Build_Process.Data.write_progress(db, state1.serial, message, build_uuid)
         Build_Process.Data.set_serial(db, worker_uuid, build_uuid, state1.serial)
       }
-      body
+      build_progress_output
       _state = state1
     }
   }