# HG changeset patch
# User wenzelm
# Date 1713278228 -7200
# Node ID 66d7a923b750b86351697cda4cdc25865bb151c4
# Parent  05cec0a3c63da36d45be9ad40821b6fbc3d84bd0
tuned;

diff -r 05cec0a3c63d -r 66d7a923b750 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Tue Apr 16 16:53:10 2024 +0200
+++ b/src/Pure/Build/store.scala	Tue Apr 16 16:37:08 2024 +0200
@@ -383,14 +383,14 @@
     server: SSH.Server = SSH.no_server
   ): Option[SQL.Database] = {
     if (database_server.isDefined) None
-    else store.maybe_open_database_server(server = server, guard = build_cluster)
+    else maybe_open_database_server(server = server, guard = build_cluster)
   }
 
   def maybe_using_heaps_database[A](
     database_server: Option[SQL.Database],
     server: SSH.Server = SSH.no_server
   )(f: SQL.Database => A): Option[A] = {
-    using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
+    using_optional(maybe_open_heaps_database(database_server, server = server)) {
       heaps_database => (database_server orElse heaps_database).map(f)
     }
   }