Re: two spaces after @pxref at end of source line

[Karl Berry]

Hi Kevin,

    Perhaps it's something to do with the .texi having the
    "(@pxref{blah,blah})" at the end of a source line.  

I suspect you are right.

I'll look at it when I can, but I don't think it'll be soon.
You might be able to work around the problem by using
@pxref{foo}@ 
... though I admit I didn't try it.

Thanks for the report.

k