#include <device/pci.h>
#include <device/pci_ids.h>
#include <cpu/x86/msr.h>
-#include "dmi.h"
extern const unsigned char AmlCode[];
#if CONFIG_HAVE_ACPI_SLIC
ALIGN_CURRENT;
printk(BIOS_DEBUG, "current = %lx\n", current);
-
- 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
-
printk(BIOS_INFO, "ACPI: done.\n");
return current;
}