| Tue, 22 Apr 2025 22:11:16 +0200 | wenzelm | tuned signature -- requires to update jedit component; | file | diff | annotate |
| 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 |