Mon, 04 Sep 2017 20:55:06 +0200 | wenzelm | tuned signature -- avoid warning during jEdit startup; | file | diff | annotate |
Mon, 04 Sep 2017 15:25:25 +0200 | wenzelm | more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache; | file | diff | annotate |
Fri, 01 Sep 2017 15:42:10 +0200 | wenzelm | clarified startup sequence; | file | diff | annotate |