Looks great, thank you so much! Chris
On Tue, Dec 15, 2020 at 12:00 PM Paul Eggert <egg...@cs.ucla.edu> wrote: > Thanks for your bug report. I installed the attached patch; although it > doesn't use the exact wording you proposed, I hope it works well enough. >