Re: [ jEdit-users ] Plugin Manager deleted my JDK's tools.jar

[Slava P. <sl...@je...>]

Do you mean tools.jar show up in the plugins list in the plugin manager,
and you accidentally deleted it? (I guess it should not be listed
there.) Or did the plugin manager just decide to blow it away for no
reason?

On Tue, 2003-10-28 at 17:54, Doug Breaux wrote:
> One thing that has bitten me with 4.2 is how the Plugin Manager can 
> actually delete your JDK's tools.jar file entirely.  The "Hide 
> libraries" checkbox helps, but it seems to me that jEdit should not 
> allow any deletion of files in the JDK lib (or ext) directory at all. 
> Can this be prevented?
> 
> 
> 
> -------------------------------------------------------
> This SF.net email is sponsored by: SF.net Giveback Program.
> Does SourceForge.net help you be more productive?  Does it
> help you create better code?   SHARE THE LOVE, and help us help
> YOU!  Click Here: http://sourceforge.net/donate/
-- 
Slava Pestov