<div dir="auto">Thanks! Looks good to me.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, May 30, 2022, 4:46 PM Paul Eggert <<a href="mailto:eggert@cs.ucla.edu">eggert@cs.ucla.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thanks for the info. I installed the attached proposed patch.</blockquote></div>