|
From: Gerd K. <ge...@bi...> - 2004-05-25 18:31:23
|
On May 23, 2004, at 11:51 PM, Slava Pestov wrote: > Gerd Knops wrote: > >> Manual says: >> >> "Additionally, plugins using the new jEdit 4.2 plugin API can be >> loaded and unloaded at any time. This is a great help when >> developing >> your own plugins -- there is no need to restart the editor after >> making >> changes." >> >> So, how does one unload/reload a plugin under development? > > > In the plugin manager. > D'ooohhh... I guess I misinterpreted the meaning of that checkbox. Thanks Gerd |