static void print_debug_pci_dev(u32 dev)
{
-#if PCI_BUS_SEGN_BITS==0
+#if CONFIG_PCI_BUS_SEGN_BITS==0
printk_debug("PCI: %02x:%02x.%02x", (dev>>20) & 0xff, (dev>>15) & 0x1f, (dev>>12) & 0x7);
#else
printk_debug("PCI: %04x:%02x:%02x.%02x", (dev>>28) & 0x0f, (dev>>20) & 0xff, (dev>>15) & 0x1f, (dev>>12) & 0x7);