On Mon, Oct 14, 2024 at 06:33:21PM +0100, Gavin Smith wrote:
> > If we continue removing the extension, it should be mentioned in the
> > manual in the HTML Xref specification, I think as an exception that
> > other implementations do not need to follow, as it should be mentioned
> > and also becau
On Wed, Jan 10, 2024 at 11:53:24PM +0100, Patrice Dumas wrote:
> Hello,
>
> Right now, a .inf or .info extension in fourth @ref/@xref... argument is
> removed to determine the manual base name for the purpose of doing cross
> references to manuals in HTML. I guess that it comes from the time when
Hello,
Right now, a .inf or .info extension in fourth @ref/@xref... argument is
removed to determine the manual base name for the purpose of doing cross
references to manuals in HTML. I guess that it comes from the time when
the manual name was an info file name and needed an extension to be
foun
