// Sorry for my previous comment, wrong window (comment already hidden) //
Current manual (with latest proposed patch) seems fine for me.
// Sorry for my previous comment, wrong window (comment already hidden) //
Current manual (with latest proposed patch) seems fine for me.