--- a/src/Pure/System/host.scala Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/System/host.scala Mon Mar 06 15:56:28 2023 +0100
@@ -114,8 +114,7 @@
def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
if (read_numa_next(db, hostname) != numa_next) {
- db.execute_statement(
- Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)))
+ 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