On Thu, Dec 08, 2022 at 01:50:17PM -0800, John Hubbard wrote: > However, of course I won't insist here, as there are clearly preferences > in both directions. And the code is still small in either form in this > case so really a non-issue. Thanks, John. -- Peter Xu