When trying to download a plugin the PluginManager
should first do a HEAD request to see if the file is
available, and then download the plugin. If not, or
if there is an error, it should automatically try
another mirror until all are tried. If none of the
mirrors worked, ask the user to try later or install
the plugins manually with a hint where he find
documentation about how to do it. Then there is no
need anymore to select the mirror manually and so the
setting can be removed.
Sorry if this is a dupe, but I have many bugs to post
and am too lazy to check them all for dupes
currently. :-)
OS: Windows XP
Java Version: Sun Java 1.5.0_09-b03
jEdit Version: 4.3pre8
| Submitted | vampire0 - 2006-11-09 16:55:42 | Assigned | |
|---|---|---|---|
| Priority | 5 | Labels | core |
| Status | open | Group | None |
| Resolution | None |