src/Tools/jEdit/patches/extended_styles_brackets
Tue, 29 Oct 2024 12:30:15 +0100 wenzelm update to jedit5.7.0;
Fri, 26 Apr 2024 19:15:37 +0200 wenzelm more robust: avoid spurious ConcurrentModificationException;
Mon, 20 Nov 2023 15:55:10 +0100 wenzelm rebuild jedit with minimal patch for jdk-21, following SVN 25690;
Mon, 10 May 2021 18:31:18 +0200 wenzelm more brackets;
less more (0) tip