printk(BIOS_DEBUG, "IOAPIC: ID = 0x%02x\n", ioapic_id);
/* Set IOAPIC ID if it has been specified. */
io_apic_write(ioapic_base, 0x00,
- (io_apic_read(ioapic_base, 0x00) & 0xfff0ffff) |
+ (io_apic_read(ioapic_base, 0x00) & 0xf0ffffff) |
(ioapic_id << 24));
}