# HG changeset patch
# User wenzelm
# Date 1678093733 -3600
# Node ID 8f464df3520a6512c7aa082b3ab62a6604bfed58
# Parent  69af424b1f9d5863df7e603c91d7c62e87683a9b
tuned;

diff -r 69af424b1f9d -r 8f464df3520a 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
     }
   }