This is the mail archive of the
gdb-patches@sourceware.org
mailing list for the GDB project.
Re: [PATCH, doc]: Rename Index node to prevent file collision
> Date: Thu, 14 Jun 2012 15:00:37 -0700
> From: Joel Brobecker <brobecker@adacore.com>
> Cc: Eli Zaretskii <eliz@gnu.org>,
> "Joseph S. Myers" <joseph@codesourcery.com>,
> gdb-patches@sourceware.org
>
> > 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...
makeinfo is no longer maintained. It will be replaced in the next
Texinfo release with a Perl-based reimplementation from scratch, which
is said to give us all kinds of wonders, and where you should ask for
this feature.
I have no idea when the next release will happen. Until then, I would
suggest that the interested parties simply hack their own copies of
makeinfo to do what you need. The code that puts several nodes on the
same HTML file and adjusts the links to DTRT is there, it just isn't
enabled on Posix platforms. Enable it, and you are home free. If you
need my help, just ask (I'm the one who adapted makeinfo to
case-insensitive filesystems years ago, and the text quoted above is
my fault).