more direct state update;
authorwenzelm
Mon, 13 Mar 2023 22:18:22 +0100
changeset 77640 9ed8b85e7d67
parent 77639 d5344cc1fae7
child 77641 4563db765eb2
more direct state update;
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
     }
   }