Re: [PATCH, doc]: Rename Index node to prevent file collision

[Joel Brobecker <brobecker@adacore.com>]

> Yip.  We supply pre-built toolchains for Linux and Windows[1].  The
> build is crtosstool-NG based, runs on Ubuntu Lucid, and uses the LSB
> compilers for Linux and the mingw cross compilers for Windows.  We
> cross-make the manuals the same as we cross-build the compiler.

I think we do something similar as well. I do not think that this is
an uncommon situation when someone works with GNU software on multiple
platforms.

> The makeinfo manual says: """If makeinfo is run on a system which does
> not distinguish case in filenames, nodes which are the same except for
> case will also be folded into the same output file.""".  I don't think
> that's valid here as the index is a special case: we shouldn't merge
> the top level index.html with the output of a node called Index.

I haven't checked, but is there a command-line option to force
that behavior? And I am also wondering why they wouldn't just
always make sure that the names are always different, irrespective
of casing...

-- 
Joel