On Mon, Jun 22, 2020 at 09:09:28PM +0200, Fabien COELHO wrote:
> Should it be backpatched? I'm not sure what the usual practice is wrt to
> small fixes in the doc.
The text is right, and this impacts only the appearance of the text,
so I did not see that this was enough for a backpatch.
--
Michael