Thanks! Looks good to me.

On Mon, May 30, 2022, 4:46 PM Paul Eggert <eggert@cs.ucla.edu> wrote:

Thanks for the info. I installed the attached proposed patch.