Menu
▾
▴
Re: [ jEdit-devel ] Docker Plug-In Auto-Hide Overrides Cannot Be Removed
|
From: Slava P. <sl...@je...> - 2003-04-29 18:22:58
|
On Tue, Apr 29, 2003 at 01:53:26PM -0400, Calvin Yu wrote: > > If you need to remove a dockable, modify the 'docker.auto-hide- > overrides' jEdit property while jEdit is closed. In fact there is no need to close jEdit; it will notice that the property file has been changed on disk and not overwrite it on exit. -- Slava Pestov |