Re: Doubled slash instead of simple slash when running makeinfo v4.13

[Karl Berry]

Hi Christophe,

    So here are simple slash "/" replaced by double ones "//", is that a

They're equivalent on modern systems, so it doesn't exactly seem like an
error to me.  It still shouldn't happen though -- and it doesn't happen
for me.  The cwd is not prepended at all, with or without the extra /

Are you running the original GNU 4.13 release, or some distro version?
Or maybe GCC is supplying its own makeinfo?  They did at one time.

Best,
Karl