Changes in kernel/arch/ia32/src/bios/bios.c [dc0b964:df4ed85] in mainline

File:

• kernel/arch/ia32/src/bios/bios.c (modified) (3 diffs)

kernel/arch/ia32/src/bios/bios.c

@@ -27 +27 @@
  */
 
-/** @addtogroup ia32
+/** @addtogroup ia32    
  * @{
  */
@@ -34 +34 @@
 
 #include <arch/bios/bios.h>
-#include <typedefs.h>
-
-#define BIOS_EBDA_PTR  0x40eU
+#include <arch/types.h>
 
 uintptr_t ebda = 0;
@@ -43 +41 @@
 {
         /* Copy the EBDA address out from BIOS Data Area */
-        ebda = *((uint16_t *) BIOS_EBDA_PTR) * 0x10U;
+        ebda = *((uint16_t *) BIOS_EBDA_PTR) * 0x10;
 }