Documentation: Fix cross reference names in PDF generation of the docs

Documentation: Fix cross reference names in PDF generation of the docs

For cross-references to other documents, one should always use the
five-argument version of @ref (where the fifth argument is the displayed
name of the other document). There won't be a reference to a particular
page, only to the section given by the node name and the name of the
other manual.