re-use cache from Main_Plugin.start;
authorwenzelm
Mon, 23 Jun 2025 14:44:59 +0200
changeset 82743 b00337cda5b9
parent 82742 085e624a1303
child 82744 0ca8b1861fa3
re-use cache from Main_Plugin.start;
src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Jun 23 14:42:40 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Jun 23 14:44:59 2025 +0200
@@ -47,7 +47,7 @@
   /* database store */
 
   def sessions_store(options: Options = PIDE.options.value): Store =
-    Store(session_options(options))
+    Store(session_options(options), cache = PIDE.cache)
 
   def open_session_context(
     store: Store = sessions_store(),