Dear all,

here's a documentation bugfix.  The previous wording was in conflict
with the standard, while the runtime behavior is apparently fine.

Checked with make dvi pdf .

OK for mainline?

Thanks,
Harald