Re: [PATCH] ignoring Info extensions

[Richard Stallman]

    I am not aware of any Info files with references without whitespace
    after `*Note'.  Perhaps somewhere such files may exist that was
    generated by a program other than makeinfo, or was hand-written?

Isn't it the case that Texinfo will always produce whitespace
after *Note when it is a cross reference?  I don't think we need
to worry very much about hand-made Info files which might fail
to have whitespace there.