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

[Doug B. <br...@cl...>]

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?