Index: kernel/arch/ia32/include/bios/bios.h
===================================================================
--- kernel/arch/ia32/include/bios/bios.h	(revision 1d3d2cf821c9a68d853e80ee2c7571d01c79b54a)
+++ kernel/arch/ia32/include/bios/bios.h	(revision be3f94cc9353d7054d4a674904c7150a2206f504)
@@ -38,6 +38,4 @@
 #include <typedefs.h>
 
-#define BIOS_EBDA_PTR  0x40e
-
 extern uintptr_t ebda;
 
Index: kernel/arch/ia32/src/bios/bios.c
===================================================================
--- kernel/arch/ia32/src/bios/bios.c	(revision 1d3d2cf821c9a68d853e80ee2c7571d01c79b54a)
+++ kernel/arch/ia32/src/bios/bios.c	(revision be3f94cc9353d7054d4a674904c7150a2206f504)
@@ -36,4 +36,6 @@
 #include <typedefs.h>
 
+#define BIOS_EBDA_PTR  0x40e
+
 uintptr_t ebda = 0;