--- a/src/Pure/System/host.scala Mon Mar 06 15:12:37 2023 +0100
+++ b/src/Pure/System/host.scala Mon Mar 06 15:38:50 2023 +0100
@@ -114,14 +114,13 @@
def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
if (read_numa_next(db, hostname) != numa_next) {
- db.using_statement(
- Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname))
- )(_.execute())
- db.using_statement(Node_Info.table.insert()) { stmt =>
- stmt.string(1) = hostname
- stmt.int(2) = numa_next
- stmt.execute()
- }
+ db.execute_statement(
+ Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)))
+ db.execute_statement(Node_Info.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = hostname
+ stmt.int(2) = numa_next
+ })
true
}
else false