src/Tools/jEdit/patches/jedit/extended_styles
Sat, 01 Dec 2012 17:23:50 +0100 wenzelm more generic directory name to facilitate tracking changes of diffs;
less more (0) tip