tuned signature;
authorwenzelm
Tue, 14 Mar 2023 18:29:07 +0100
changeset 77655 136ab737a36d
parent 77654 78913f29fc21
child 77656 fd553b54fce1
tuned signature;
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)