# HG changeset patch
# User wenzelm
# Date 1678742302 -3600
# Node ID 9ed8b85e7d67a28bed6f5509e90dfd487af70c76
# Parent  d5344cc1fae71a1d6bad6878247c86742a129af3
more direct state update;

diff -r d5344cc1fae7 -r 9ed8b85e7d67 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 13 22:08:46 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 13 22:18:22 2023 +0100
@@ -874,13 +874,12 @@
 
   private def progress_output(message: Progress.Message, build_progress_output: => Unit): Unit = {
     synchronized_database {
-      val state1 = _state.inc_serial.progress_serial()
+      _state = _state.inc_serial.progress_serial()
       for (db <- _database) {
-        Build_Process.Data.write_progress(db, state1.serial, message, build_uuid)
-        Build_Process.Data.stamp_worker(db, worker_uuid, state1.serial)
+        Build_Process.Data.write_progress(db, _state.serial, message, build_uuid)
+        Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial)
       }
       build_progress_output
-      _state = state1
     }
   }