On Tue, 04 Jun 2024 19:37:51 +0200, Omar Polo wrote:

> ping.  I'm positively convinced that the diff is correct, but would like
> a confirmation :)

Yes, that looks good to me.  OK millert@

 - todd