On 20.11.2012 16:05, Makarius wrote:
What might happen before the release is a move from Sidekick/completion subplugin, to the new Completion standalone-plugin from the jEdit guys. It depends if their release schedule recovers after the summer break -- I don't see any important activity there since 01-Sep-2012, whicj was the original plan for jEdit 5.0 to be rolled out.
It seems to have recovered just half an hour ago. -- Lars _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
