Hello!

I believe commit 13fb25ba0c24a9e7732d2c32dbc882c7d462bce9 (pasted below)
fixes that.  Can you confirm?

Thanks,
Ludo’.