src/Tools/jEdit/patches/status_bar
Wed, 23 Apr 2025 13:32:16 +0200 wenzelm clarified patches;
less more (0) tip