Re: Doc fixes for makeinfo --html

[Eli Zaretskii <eliz@gnu.org>]

> Date: Wed, 14 Jan 2009 11:30:50 +0000 (UTC)
> From: "Joseph S. Myers" <joseph@codesourcery.com>
> cc: gdb-patches@sourceware.org
> 
> On Wed, 14 Jan 2009, Eli Zaretskii wrote:
> 
> > > * To work on case-insensitive filesystems with makeinfo splitting by
> > >   node, the index should not be called "Index" as this clashes with
> > >   the automatically generated index.html.
> > 
> > In what version of makeinfo did you see this problem, and on what OS
> > and which port?  Because it was solved long ago: when some <node>.html
> > clashes with another <node>.html, makeinfo should resolve the clash
> > automatically.
> 
> Various versions of makeinfo up to 4.12.  The problem is building GDB on 
> i686-pc-linux-gnu (build system) with --host=i686-mingw32; I have not 
> tried any version of makeinfo running directly on the case-insensitive 
> systems

That might explain it: I think the feature I was talking about only
works on DOS and Windows, where the problem happens.

> There is no way to pass the expected host to makeinfo, and since 
> documentation goes in a "share" directory the files generated should not 
> depend at all on the host in any case; it would be a bug for the files in 
> the share directory to differ for different --host configurations.

That's quite an unusual setup for producing Info files; I'm not sure
GDB should make changes in the manual to cater to it.

My suggestion would be to add an option to makeinfo to enable the
feature on any platform, or maybe run makeinfo on Windows to produce
these files.