On Tue, Oct 22, 2024 at 8:48 AM Thomas Passin <[email protected]> wrote:

> Hah! I see it's been done.  Good!
>

Now I'm confused. What has been done? PR #4111
<https://github.com/leo-editor/leo-editor/pull/4111> has not been merged,
but I'll accept the PR once I'm a bit less confused.

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 [email protected].
To view this discussion on the web visit 
https://groups.google.com/d/msgid/leo-editor/CAMF8tS3J9U7kByHUEW%2BMbcwAdvr7yt-scCUNtENaon07%3DLLSPQ%40mail.gmail.com.

Reply via email to