Here is a trivial documentation fix for some of recent PCI hotplug changes
that enables 'make htmldocs' to complete.