[ jEdit-users ] Suggestion for installer: specify plugin dir

[Dirk M. <dmo...@gm...>]

Hello,

I have a suggestion for the jedit installer:
Let the user specify a seperate directory for the plugins (on step 2 of
the install process). Defaulting to <jedit-installdir>/jars.

The installer will look, whether the directory already exists and
whether there are any old plugins. He will overwrite any plugins, for
which he delivers new versions (that would be LatestVersion,
PluginManager and Firewall in most cases).

That way I could maintain my plugins in a seperate dir and wouldn't be
forced to copy them on each new jEdit release.

What do you think about it?


Dirk.