On Tue, 2023-06-13 at 10:57 +0000, Oliver Marienfeld wrote: > I would understand if you decided against extending the docs.
I don't get to decide that. If you come up with a patch for the documentation, that would increase the chances that the documentation actually gets changed. Yours, Laurenz Albe