src/Tools/jEdit/patches/gui
Wed, 14 May 2025 11:31:23 +0200 wenzelm simplified structure of patches;
less more (0) tip