Re: local header name assigned to system header float.h

[Karl Berry]

    It may be harmless to have a local header with the same name as a
    system header, or it is not.

Thanks for the suggestion.  I suppose I can imagine vague circumstances
where it might cause a problem, although it never has in practice.
Meanwhile, it doesn't matter, since the C implementation of makeinfo has
been discontinued and will no longer be maintained or distributed.

Best,
karl