author | wenzelm |
Mon, 23 Jun 2025 14:44:59 +0200 | |
changeset 82743 | b00337cda5b9 |
parent 82742 | 085e624a1303 |
child 82744 | 0ca8b1861fa3 |
--- 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(),