[ jEdit-devel ] Plugin uninstall

[Matthieu C. <cho...@gm...>]

Hi, I think the plugin api is missing something : uninstallation.
Several plugins write files in the settings directory, but those files
aren't removed when removing plugins.
We should also rationalize the settings of the plugins.
Maybe a method could return the path where the plugins could write their
settings, this name would be something like
settingsDirectory/plugins/pluginName
and when removing a plugin, jEdit would ask if the user wants to delete the
settings of the plugin or keep them.
By default removing those settings would only remove this folder, but the
plugin could overwrite the method to do some different job

Matthieu