On Saturday 28 August 2004 20:46, Slava Pestov wrote:
> Hello everybody,
> This is it. jEdit 4.2final is now available from
Congratulations and thanks to you and all contributors.
> List of changes since 4.1final: <http://www.jedit.org/42docs/news42/>.
> List of changes since 4.2pre15: <http://www.jedit.org/CHANGES42.txt>.
> If you're upgrading from 4.1, remove all your plugins and download a
> fresh set from within 4.2.
If I'm running, say, 4.2pre14, can I just copy over the files from my
current .../jars/ directory (those that are not already present in the
base install of 4.2final)? Or is it recommended that I use the plug-in
manager and download everything anew?
> Have fun.
I will. jEdit's the best.
Again, thanks for all the hard work (and for taking out arrow key handling
in the search bar)