diff --git a/sys/dev/pci/pci.c b/sys/dev/pci/pci.c index d9a5e626a11b..053cf58da2d7 100644 --- a/sys/dev/pci/pci.c +++ b/sys/dev/pci/pci.c @@ -919,7 +919,8 @@ pci_add_resources(device_t pcib, device_t bus, device_t dev) } if (cfg->intpin > 0 && PCI_INTERRUPT_VALID(cfg->intline)) { -#if defined(__ia64__) || defined(__i386__) || defined(__amd64__) +#if defined(__ia64__) || defined(__i386__) || defined(__amd64__) || \ + defined(__arm__) /* * Try to re-route interrupts. Sometimes the BIOS or * firmware may leave bogus values in these registers.