# HG changeset patch
# User wenzelm
# Date 1692799143 -7200
# Node ID 980f3cfcbc2c3f42a98f1e8b101b1b15c9cf5bc7
# Parent  11cf77478d3ed11e6aea16355b4765382ffbfae2
more accurate treatment of state vs. serial vs. db;

diff -r 11cf77478d3e -r 980f3cfcbc2c src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Aug 23 14:23:41 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Aug 23 15:59:03 2023 +0200
@@ -54,7 +54,6 @@
     node_info: Host.Node_Info,
     build: Option[Build_Job]
   ) extends Library.Named {
-    def no_build: Job = copy(build = None)
     def join_build: Option[Build_Job.Result] = build.flatMap(_.join)
   }
 
@@ -641,7 +640,7 @@
       old_running: State.Running
     ): Boolean = {
       val running0 = old_running.valuesIterator.toList
-      val running1 = running.valuesIterator.map(_.no_build).toList
+      val running1 = running.valuesIterator.toList
       val (delete, insert) = Library.symmetric_difference(running0, running1)
 
       if (delete.nonEmpty) {
@@ -807,8 +806,11 @@
       val serial0 = state.serial
       val serial = if (changed.exists(identity)) State.inc_serial(serial0) else serial0
 
-      stamp_worker(db, worker_uuid, serial)
-      state.set_serial(serial)
+      if (serial0 != serial) {
+        stamp_worker(db, worker_uuid, serial)
+        state.set_serial(serial)
+      }
+      else state
     }
   }