On Feb 23, 2023, at 11:03 AM, Axel Rasmussen axelrasmussen@google.com wrote:
Oh! I must have missed it, or just forgot. I'll take a look and see about making some improvements. I'll also be sure to credit you in the commit message.
It was not about credit. I just wanted to refer you to what I had in mind, and David did spend some time on reviewing my patch...
;-)