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
