On Tue, 13 Jun 2023 at 23:29, Pavel Stehule <pavel.steh...@gmail.com> wrote: >> I think it's probably worth adjusting the docs to mention this. It >> seems like it might be something that could surprise someone. >> >> Something like the attached, maybe? > > +1
Ok, I pushed that patch. Thanks. David
