do not remove .inf or .info in @ref manual name argument to construct HTML ref

[Patrice Dumas]

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
found, a time long gone.

I propose that we stop removing that extension, because nowadays it is
better if manuals are fixed instead, because we do not do that for other
output formats and because it is not documented in the HTML Xref
specification:
https://www.gnu.org/software/texinfo/manual/texinfo/html_node/HTML-Xref-Link-Basics.html

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 because it makes texi2any non conforming to the HTML Xref
specification.

Any oppostion to stopping removing the extension?

-- 
Pat