| Sun, 11 May 2014 20:23:08 +0200 | wenzelm | more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion; | file | diff | annotate |
| Thu, 08 May 2014 00:14:06 +0200 | wenzelm | some odd tricks to provide "Detach" menu item, via "PIDE" docking framework; | file | diff | annotate |