# HG changeset patch
# User wenzelm
# Date 1678814947 -3600
# Node ID 136ab737a36d52d809553f0470d2d7bcdf414685
# Parent  78913f29fc216df92a7248c0a0d6372b7e1b7158
tuned signature;

diff -r 78913f29fc21 -r 136ab737a36d src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 17:34:38 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 18:29:07 2023 +0100
@@ -542,6 +542,12 @@
       val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
     }
 
+    def read_serial(db: SQL.Database): Long =
+      db.execute_query_statementO[Long](
+        Workers.table.select(List(Workers.serial_max)),
+        res => res.long(Workers.serial)
+      ).getOrElse(0L)
+
     def read_workers(
       db: SQL.Database,
       build_uuid: String = "",
@@ -565,12 +571,6 @@
           })
     }
 
-    def serial_max(db: SQL.Database): Long =
-      db.execute_query_statementO[Long](
-        Workers.table.select(List(Workers.serial_max)),
-        res => res.long(Workers.serial)
-      ).getOrElse(0L)
-
     def start_worker(
       db: SQL.Database,
       worker_uuid: String,
@@ -832,10 +832,10 @@
       hostname: String,
       state: State
     ): State = {
-      val serial0 = serial_max(db)
-      if (serial0 == state.serial) state
+      val serial_db = read_serial(db)
+      if (serial_db == state.serial) state
       else {
-        val serial = serial0 max state.serial
+        val serial = serial_db max state.serial
         stamp_worker(db, worker_uuid, serial)
 
         val numa_next = Host.Data.read_numa_next(db, hostname)