# HG changeset patch
# User wenzelm
# Date 1686228331 -7200
# Node ID 2fdf3d8a94e6bb27933a1f7426a87aac89b25ef6
# Parent  b7b777fc916cf641ef2c9ccf85a6d384a08ae840
clarified signature;

diff -r b7b777fc916c -r 2fdf3d8a94e6 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Jun 07 17:09:17 2023 +0200
+++ b/src/Pure/General/sql.scala	Thu Jun 08 14:45:31 2023 +0200
@@ -152,6 +152,8 @@
     def where_equal(s: String): Source = SQL.where(equal(s))
     def where_member(set: Iterable[String]): Source = SQL.where(member(set))
 
+    def max: Column = copy(expr = "MAX(" + ident + ")")
+
     override def toString: Source = ident
   }
 
diff -r b7b777fc916c -r 2fdf3d8a94e6 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Jun 07 17:09:17 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Thu Jun 08 14:45:31 2023 +0200
@@ -576,13 +576,11 @@
 
       val table = make_table("workers",
         List(worker_uuid, build_uuid, hostname, java_pid, java_start, start, stamp, stop, serial))
-
-      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)), _.long(Workers.serial)).getOrElse(0L)
+        Workers.table.select(List(Workers.serial.max)), _.long(Workers.serial)).getOrElse(0L)
 
     def read_workers(
       db: SQL.Database,