src/Tools/jEdit/src/plugin.scala
changeset 58928 23d0ffd48006
parent 57979 fc136831d6ca
child 59077 7e0d3da6e6d8
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Nov 07 16:22:25 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Nov 07 16:36:55 2014 +0100
     1.3 @@ -261,7 +261,7 @@
     1.4          }
     1.5  
     1.6        case Session.Ready =>
     1.7 -        PIDE.session.update_options(PIDE.options.value)
     1.8 +        PIDE.session.init_options(PIDE.options.value)
     1.9          PIDE.init_models()
    1.10  
    1.11          if (!Isabelle.continuous_checking) {