src/Pure/System/host.scala

--- a/src/Pure/System/host.scala	Sun Mar 05 18:38:52 2023 +0100
+++ b/src/Pure/System/host.scala	Sun Mar 05 19:21:07 2023 +0100
@@ -98,25 +98,25 @@
 
     object Node_Info {
       val hostname = SQL.Column.string("hostname").make_primary_key
-      val numa_index = SQL.Column.int("numa_index")
+      val numa_next = SQL.Column.int("numa_next")
 
-      val table = make_table("node_info", List(hostname, numa_index))
+      val table = make_table("node_info", List(hostname, numa_next))
     }
 
-    def read_numa_index(db: SQL.Database, hostname: String): Int =
+    def read_numa_next(db: SQL.Database, hostname: String): Int =
       db.using_statement(
-        Node_Info.table.select(List(Node_Info.numa_index),
+        Node_Info.table.select(List(Node_Info.numa_next),
           sql = Node_Info.hostname.where_equal(hostname))
-      )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_index)).nextOption.getOrElse(0))
+      )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_next)).nextOption.getOrElse(0))
 
-    def update_numa_index(db: SQL.Database, hostname: String, numa_index: Int): Boolean =
-      if (read_numa_index(db, hostname) != numa_index) {
+    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_index
+          stmt.int(2) = numa_next
           stmt.execute()
         }
         true