src/Tools/jEdit/patches/accelerator_font
2 months ago ago formal update of patches -- no change of content;
5 months ago ago proper menu accelerator font for Java 11 (no update of jedit-build component yet);