jEdit / Merge Requests / #197 Fix for plugins that cannot be removed

#197 Fix for plugins that cannot be removed

Milestone: for 5.2.x

Status: closed-accepted

Labels: None

Priority: 5

Updated: 2014-07-31

Created: 2014-07-29

Private: No

Please merge 23626 to fix unloaded plugins that cannot be removed on Windows

Alan Ezust - 2014-07-31

Committed 23638.

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