src/Tools/jEdit/src/jedit_resources.scala
changeset 59077 7e0d3da6e6d8
parent 57841 e212e2001b2a
child 59078 cf255dc2b48f
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Dec 01 19:25:20 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Dec 02 14:16:56 2014 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4  
     1.5    override def commit(change: Session.Change)
     1.6    {
     1.7 -    if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() }
     1.8 +    if (!change.syntax_changed.isEmpty) GUI_Thread.later { jEdit.propertiesChanged() }
     1.9      if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
    1.10    }
    1.11  }