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

[Michael Hope <michael.hope@linaro.org>]

On 15 June 2012 19:35, Eli Zaretskii <eliz@gnu.org> wrote:
>> 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.

This isn't ideal.  The problem has been discussed multiple times over
four years, affects at least four groups, and might be fixed by a
rewrite that might come out in the future.

Changing the node name works around a tools problem and makes the
output the same for all hosts.  I agree that 'Index' is more natural
than 'GDB Index'.  How about matching GCC, and call it the 'Concept
Index' instead?

-- Michael