-
- printk(BIOS_DEBUG, "ACPI: * DMI (Linux workaround)\n");
- memcpy((void *)0xfff80, dmi_table, DMI_TABLE_SIZE);
-#if CONFIG_WRITE_HIGH_TABLES == 1
- memcpy((void *)current, dmi_table, DMI_TABLE_SIZE);
- current += DMI_TABLE_SIZE;
- ALIGN_CURRENT;
-#endif
-