Tue, 05 Sep 2017 17:07:42 +0200 | nipkow | introduced bst_wrt | changeset | files |
Tue, 05 Sep 2017 16:45:23 +0200 | wenzelm | less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128); | changeset | files |
Tue, 05 Sep 2017 14:29:43 +0200 | wenzelm | tolerate more errors (cf. 1e5ae735e026); | changeset | files |
Mon, 04 Sep 2017 20:55:06 +0200 | wenzelm | tuned signature -- avoid warning during jEdit startup; | changeset | files |
Mon, 04 Sep 2017 15:25:25 +0200 | wenzelm | more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache; | changeset | files |
Sun, 03 Sep 2017 16:35:34 +0200 | wenzelm | updated for release; | changeset | files |