On Fri, 2022-10-07 at 21:37 -0700, Paul Eggert wrote: > On 10/7/22 05:36, Eli Zaretskii wrote: > > I'd appreciate a more high-level description of the idea of the > > change, in addition to the gory details. > > I gave it a shot in the attached patch, which is an improved version > of the previous patch.
I ended up doing something different but hopefully equivalent.
