Re: htmlxref.cnf vs. manual names with a dot

[Patrice Dumas]

On Sun, May 05, 2019 at 08:00:31PM +0100, Gavin Smith wrote:
> 
> I don't know for sure what the justification is 
> for that, but I suspect it is because some Texinfo manuals in the past 
> have used a file extension inside the cross-reference commands, like 
> this: @xref{node,,, manual.info, Manual}.

I think that it was done that way in makeinfo in C, so I did it
like that too.  I have checked that it is not documented, so changing it
would be ok.  The change you propose may break some manual, but the
authors should probably fix the texinfo source instead.  We could even
consider not removing .info, since we are changing what we do, as I
believe that it is better not to specify an extension in the 'info file
name' argument of @*ref.  I also think that we should change the manual
such that it is not 'info file name' but simply 'file name'.

-- 
Pat