src/Tools/jEdit/patches/props
2 months ago ago formal update of patches -- no change of content;
13 months ago ago updated to jedit-5.5.0;
2017-03-19 ago updated to jedit-5.4.0;