PR #4047 <https://github.com/leo-editor/leo-editor/pull/4047> has been merged into devel. It has also been merged (with difficulty!) into PR #4033 <https://github.com/leo-editor/leo-editor/pull/4033>, which adds new layouts.
I have taken this step now because it seems likely I shall undergo yet another surgery on my right eye. I wanted to do the complicated merges now, while most of the details are fresh in my mind. I would also like to merge #4033 today, so we can all test the new code while I recuperate. Edward -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to leo-editor+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/leo-editor/6cf7790d-f12c-4604-abc8-b37ce64b64ffn%40googlegroups.com.
