Plugins may use this general tool for uninstallation and eventually
removal of the deployed source code. At the moment, this is implemented
as a wrapper for the core function uninstall_plugin() with an extra hook
in the relevant plugin info subclass.
For non-standard add-ons, the tool can remove the deployed plugin source
code as well, if the web server has required write permissions. Ideally,
all add-ons installed via the new tool_installaddon should be removable
via the web interface as well.
436d94478d