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
