# HG changeset patch
# User wenzelm
# Date 1750682699 -7200
# Node ID b00337cda5b9e01b149fe31ffd98b5255c0d2961
# Parent  085e624a1303e0572165d7c6eba8ad375284eba1
re-use cache from Main_Plugin.start;

diff -r 085e624a1303 -r b00337cda5b9 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(),