--- 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,