On 10/3/22 13:37, Michael Albinus wrote:
> OK. Would you like to provide a patch? Including a ChangeLog-like commit
> message.

Is this okay?

-bjc