| Tue, 24 Nov 2015 22:50:03 +0100 | wenzelm | paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement); | file | diff | annotate |
| Fri, 23 Oct 2015 21:03:16 +0200 | wenzelm | updated to jedit-5.3.0 and SideKick 1.8; | file | diff | annotate | base |