Perhaps it could be added to NEWS as a "deliberate
discrepancy"?
Yes, I will.
I imagine there are many generated documents
I doubt it is all that "many", since the manual always more or less
implicitly recommended putting in blank lines in the source document
where you wanted them, and in practice, from what I've seen, that's what
people have done. And the first incarnation of makeinfo
(texinfo-format-buffer, umpteen years ago now, but many manuals date
from that time) certainly didn't put in blank lines.
k
