--- 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
}
}