On 14/04/2020 00:22, Vincent Legoll wrote:
> Hello,
>
>
> as I recently worked on the same subject in [1],
>
> I reviewed and amended the documentation patch [2].
>
>
> [1] https://debbugs.gnu.org/cgi/bugreport.cgi?bug=40601
>
> [2] https://debbugs.gnu.org/cgi/bugreport.cgi?bug=37624
>

And now with the patch...