| Tue, 29 Oct 2024 12:30:15 +0100 | wenzelm | update to jedit5.7.0; | file | diff | annotate |
| Mon, 01 Feb 2021 18:12:44 +0100 | wenzelm | avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30); | file | diff | annotate |