tuned;
authorwenzelm
Tue, 24 Jun 2025 22:17:35 +0200
changeset 82754 6204f51104da
parent 82753 5d036f258f28
child 82755 788d7f3caa41
tuned;
src/Pure/Build/build.scala
src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Pure/Build/build.scala	Tue Jun 24 22:11:04 2025 +0200
+++ b/src/Pure/Build/build.scala	Tue Jun 24 22:17:35 2025 +0200
@@ -786,8 +786,8 @@
     metric: Pretty.Metric = Symbol.Metric,
     unicode_symbols: Boolean = false
   ): Unit = {
-    val store = Store(options)
     val session = new Session(options)
+    val store = session.store
 
     def check(filter: List[Regex], make_string: => String): Boolean =
       filter.isEmpty || {
--- a/src/Tools/Find_Facts/src/find_facts.scala	Tue Jun 24 22:11:04 2025 +0200
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Tue Jun 24 22:17:35 2025 +0200
@@ -625,7 +625,6 @@
     browser_info: Boolean = true,
     progress: Progress = new Progress
   ): Unit = {
-    val store = Store(options)
     val solr = Solr.init(solr_data_dir)
     val database = options.string("find_facts_database_name")
     val session = Session(options)
@@ -643,7 +642,7 @@
         val props = meta_info(if (browser_info) Some(Path.basic("browser_info.db")) else None)
         val stats =
           using(solr.init_database(database, Find_Facts.private_data, props, clean = true)) { db =>
-            using(Export.open_database_context(store)) { database_context =>
+            using(Export.open_database_context(session.store)) { database_context =>
               val document_info = Document_Info.read(database_context, deps, sessions)
               val context1 =
                 Browser_Info.context(sessions_structure, root_dir = root_dir,