src/Tools/jEdit/patches/docking
3 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;
2015-02-28 ago updated to jedit-5.2.0;
2014-05-11 ago more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;