<p dir="ltr">Yes, this change is correct. I stumbled over this myself this afternoon.</p>
<p dir="ltr">I changed the name pretty late before submitting the patches and apparently mused some occurrences in the docs:-(</p>
<p dir="ltr">Best regards,<br>
Tobias</p>
<p dir="ltr">Sylvain: Thanks for noticing and sending in patches to correct the mistakes you found!</p>