Re: Generated GDB documentation have colliding files on a case insensitive files system

Eli Zaretskii via Gdb-patches
2023-01-15T18:10:06Z

> Date: Sun, 15 Jan 2023 18:43:53 +0100
> CC: <gdb-patches@sourceware.org>
> From: Torbjorn SVENSSON <torbjorn.svensson@foss.st.com>
>
> On 2023-01-15 18:39, Eli Zaretskii wrote:
> >> Date: Sun, 15 Jan 2023 18:22:54 +0100
> >> CC: <gdb-patches@sourceware.org>
> >> From: Torbjorn SVENSSON <torbjorn.svensson@foss.st.com>
> >>
> >> As I see it, there are 3 different options for the documentation in GDB:
> >>
> >> 1. Leave everything as is and forget about all users extracting a cross
> >> built GDB with documentation and let the users deal with duplicated files...
> >>
> >> 2. Set the CASE_INSENSITIVE_FILENAMES option and also change one of the
> >> anchors to have unique files. This will require Texinfo >7.0.1 that is
> >> not yet released.
> >>
> >> 3. Generate one single big HTML file. This should be supported with
> >> existing versions of Texinfo, although I haven't tested this option.
> >> What would be needed in GDB sources is to replace the command line
> >> option --split-size with --no-split to avoid generating more than one file.
> >>
> >>
> >> What option would you prefer?
> >
> > I think we should rename one of the anchors, and otherwise leave
> > things at that, because doing so will resolve the problem even without
> > using CASE_INSENSITIVE_FILENAMES and without waiting for a future
> > release of Texinfo, right?
>
> I suppose that would work, but there would be no indication of a
> potential future clash. Maybe that's okay anyway?

There's any number of potential problems that could potentially happen
in the future. If we start worrying about all of them, we will have
no time to do anything useful. Let's worry about problems that really
happen when they happen.