tuned;
authorwenzelm
Tue, 16 Apr 2024 16:37:08 +0200
changeset 80122 66d7a923b750
parent 80121 05cec0a3c63d
child 80123 7e4c3bb3d062
tuned;
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)
     }
   }