src/Tools/jEdit/src-base/plugin.scala
Mon, 04 Sep 2017 20:55:06 +0200 wenzelm tuned signature -- avoid warning during jEdit startup;
Mon, 04 Sep 2017 15:25:25 +0200 wenzelm more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache;
Fri, 01 Sep 2017 15:42:10 +0200 wenzelm clarified startup sequence;
less more (0) -3 tip