src/Tools/jEdit/patches/folding
4 months ago ago formal update of patches -- no change of content;
15 months ago ago updated to jedit-5.5.0;
2017-03-19 ago updated to jedit-5.4.0;
2015-10-23 ago updated to jedit-5.3.0 and SideKick 1.8;
2015-02-28 ago updated to jedit-5.2.0;
2014-10-18 ago always apply precedingFoldLevels, avoid unclear shortcuts;