# HG changeset patch # User wenzelm # Date 1750848695 -7200 # Node ID da8ad15919851ef1d372226314c6924ec287f88a # Parent a07ca02ac456e72d8c146c64a1c454c057661d50 more accurate ML_Settings from underlying Session; diff -r a07ca02ac456 -r da8ad1591985 src/Tools/jEdit/src/main_plugin.scala --- a/src/Tools/jEdit/src/main_plugin.scala Wed Jun 25 12:43:37 2025 +0200 +++ b/src/Tools/jEdit/src/main_plugin.scala Wed Jun 25 12:51:35 2025 +0200 @@ -52,8 +52,7 @@ def options: JEdit_Options = plugin.options def session: JEdit_Session = plugin.session def resources: JEdit_Resources = session.resources - - def ml_settings: ML_Settings = ML_Settings(plugin.startup_options) + def ml_settings: ML_Settings = session.store.ml_settings object editor extends JEdit_Editor }