#180 Patch for saving/restoring sessions in the session plugin

[Edward Diener]

This is a patch for correctly saving and restoring sessions for the Jedit sessions plugin. It also fixes a bug where the plugin menu item of "Save Session" was not working because the Session Manager member function had been removed. With this patch sessions are saved and restored correctly. This patch also supports sessions being saved and restored correctly when different views have different sessions.

[Alan Ezust]

Is there a bug ID# for the related bug this one fixes?

[Edward Diener]

On 9/11/2016 11:16 AM, Alan Ezust wrote:

Is there a bug ID# for the related bug this one fixes?

Can't you see '[plugin-patches:#180]' below ?

---

[plugin-patches:#180]
https://sourceforge.net/p/jedit/plugin-patches/180/ Patch for
saving/restoring sessions in the session plugin

Status: open
Created: Sat Aug 27, 2016 09:39 PM UTC by Edward Diener
Last Updated: Sun Sep 11, 2016 03:15 PM UTC
Owner: Alan Ezust
Attachments:

• sessions.patch
  https://sourceforge.net/p/jedit/plugin-patches/180/attachment/sessions.patch
  (6.4 kB; text/x-diff)

This is a patch for correctly saving and restoring sessions for the
Jedit sessions plugin. It also fixes a bug where the plugin menu item of
"Save Session" was not working because the Session Manager member
function had been removed. With this patch sessions are saved and
restored correctly. This patch also supports sessions being saved and
restored correctly when different views have different sessions.

[Alan Ezust]

Committed revision 24530.

[Matthew Gavin]

I see this bug was fixed in August 2016 but the plugin available at https://sourceforge.net/projects/jedit-plugins/ is dated January 2015. Where can I find a sessions.jar for jEdit with this, and any other later, bug fixes? Thanks in advance