This may break linking on GitHub, but it's more important for the
links to work in the documentation generated by rdoc.

Fixes [Bug #14743]