Re: [ jEdit-devel ] jEdit Plugin Removal Bug

[Dale A. <da...@ge...>]

If you uncheck the "Hide libraries" box, the plugin will still be 
visible in the list when you uncheck the box by the plugin. So 
unchecking the box by the plugin unloads it, then checking it again 
reloads it, which is handy when you're developing a plugin.

Dale


Wilson Jimmy - jiwils wrote:
> Wow!  I feel foolish.  I never noticed the "Remove" button before now.
> Thanks for your help!
> 
> Does this mean that the purpose of the checkbox is  to "remove" a plugin for
> a given jEdit session (possibly for reloading)?  After I uncheck that box,
> the plugin disappears from the list.
> 
> Jimmy