Bug#484740: some cross references don't work as info search files without .info extension

[Vincent Lefevre <vincent@vinc17.org>]

As a workaround, one can add the .info extension explicitly, e.g.
(from mpfr.texi -- MPFR trunk):

@pxref{Formatted Output Strings,,, gmp.info,GNU MP}.

instead of

@pxref{Formatted Output Strings,,, gmp,GNU MP}.

but when generating HTML and PDF files, the texinfo tools forget
to remove this extension. So, one needs to use @ifinfo (to use
the version with the .info extension) and @ifnotinfo (to use the
version without the extension, or alternatively disable the links,
as these links are often incorrect due to the absence of a search
mechanism for HTML and PDF).

-- 
Vincent Lefèvre <vincent@vinc17.org> - Web: <http://www.vinc17.org/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.org/blog/>
Work: CR INRIA - computer arithmetic / Arenaire project (LIP, ENS-Lyon)