# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1697653562 -7200
# Node ID c7f436a63108861abff5d5d1cb211827cf97fae0
# Parent  fc3ba0a1c82f622cc709f2e64869a4afae885b44
always use host database and make protected;

diff -r fc3ba0a1c82f -r c7f436a63108 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Oct 18 20:12:07 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Oct 18 20:26:02 2023 +0200
@@ -886,8 +886,8 @@
     build_options.seconds(option)
   }
 
-  private val _host_database: Option[SQL.Database] =
-    try { store.maybe_open_build_database(path = Host.private_data.database, server = server) }
+  protected val _host_database: SQL.Database =
+    try { store.open_build_database(path = Host.private_data.database, server = server) }
     catch { case exn: Throwable => close(); throw exn }
 
   protected val (progress, worker_uuid) = synchronized {
@@ -927,7 +927,7 @@
   def close(): Unit = synchronized {
     Option(_database_server).flatten.foreach(_.close())
     Option(_build_database).flatten.foreach(_.close())
-    Option(_host_database).flatten.foreach(_.close())
+    Option(_host_database).foreach(_.close())
     Option(_build_cluster).foreach(_.close())
     progress match {
       case db_progress: Database_Progress => db_progress.exit(close = true)
@@ -987,11 +987,7 @@
   protected def next_node_info(state: Build_Process.State, session_name: String): Host.Node_Info = {
     def used_nodes: Set[Int] =
       Set.from(for (job <- state.running.valuesIterator; i <- job.node_info.numa_node) yield i)
-    val numa_node =
-      for {
-        db <- _host_database
-        n <- Host.next_numa_node(db, hostname, state.numa_nodes, used_nodes)
-      } yield n
+    val numa_node = Host.next_numa_node(_host_database, hostname, state.numa_nodes, used_nodes)
     Host.Node_Info(hostname, numa_node, Nil)
   }