Use the dev_printk-like "%04x:%02x" format for printing PCI bus numbers.
Signed-off-by: Bjorn Helgaas <bjorn.helgaas@hp.com>
Signed-off-by: Jesse Barnes <jbarnes@virtuousgeek.org>