--- 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,