jEdit / Bugs / #3877 If a plugin is unloaded, it is impossible to remove it

#3877 If a plugin is unloaded, it is impossible to remove it

Milestone: normal bug

Status: closed-fixed

Owner: Matthieu Casanova

Labels: Windows Specific (129)

Priority: 9

Updated: 2014-07-31

Created: 2014-07-28

Creator: Matthieu Casanova

Private: No

When a plugin is removed, the plugin manager generates it's cache but do not close the zip file, so the jar is locked and the plugin will not be removable (at least on Windows)

Bugs: ~~#3878~~

Discussion

Matthieu Casanova - 2014-07-28

status: open --> closed-fixed
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Matthieu Casanova - 2014-07-28

Fixed in [r23626]

Related

Commit: [r23626]

Last edit: Björn Kautler 2014-08-13

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

If a plugin is unloaded, it is impossible to remove it

jEdit is a programmer's text editor written in Java.

Group

Searches

Help

#3877 If a plugin is unloaded, it is impossible to remove it

Related

Discussion

Related