# HG changeset patch
# User wenzelm
# Date 1710238718 -3600
# Node ID ede8b298cfe89cef3b3f0180e9cde3b5c0ed48a8
# Parent  741b52cb497c78e5368ed8e6a9f9133a7881e66b
tuned signature;

diff -r 741b52cb497c -r ede8b298cfe8 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Mar 12 11:16:06 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Tue Mar 12 11:18:38 2024 +0100
@@ -230,7 +230,6 @@
     results: State.Results = Map.empty
   ) {
     def next_serial: Long = State.inc_serial(serial)
-    def inc_serial: State = copy(serial = next_serial)
 
     def ready: List[Task] = pending.valuesIterator.filter(_.is_ready).toList.sortBy(_.name)
     def next_ready: List[Task] = ready.filter(entry => !is_running(entry.name))
@@ -1265,7 +1264,7 @@
 
   protected final def start_worker(): Unit = synchronized_database("Build_Process.start_worker") {
     for (db <- _build_database) {
-      _state = _state.inc_serial
+      _state = _state.copy(serial = _state.next_serial)
       Build_Process.private_data.start_worker(db, worker_uuid, build_uuid, _state.serial)
     }
   }