This is the mail archive of the
mailing list for the GDB project.
Re: [PATCH, doc]: Rename Index node to prevent file collision
- From: "Joseph S. Myers" <joseph at codesourcery dot com>
- To: Michael Hope <michael dot hope at linaro dot org>
- Cc: gdb-patches at sourceware dot org
- Date: Thu, 14 Jun 2012 15:06:30 +0000 (UTC)
- Subject: Re: [PATCH, doc]: Rename Index node to prevent file collision
- References: <4FD94EC0.firstname.lastname@example.org>
On Thu, 14 Jun 2012, Michael Hope wrote:
> Hi there. This patch renames the 'Index' node in the GDB end user
> documentation to 'GDB Index'
> to prevent generating HTML filenames that differ only in case.
This was rejected when I submitted it
Joseph S. Myers