Re: [ jEdit-devel ] Unloading plugins?

[Gerd K. <ge...@bi...>]

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