src/Tools/jEdit/patches/docking
Sun, 19 Mar 2017 20:28:21 +0100 wenzelm updated to jedit-5.4.0;
Sat, 28 Feb 2015 21:51:34 +0100 wenzelm updated to jedit-5.2.0;
Sun, 11 May 2014 20:23:08 +0200 wenzelm more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
less more (0) tip