:: commit 5ee65db085aa2fcc8c19f6ef51ad3b20a28ad997

diff --git a/common/entry.s2.c b/common/entry.s2.c
index 9de0697f..b553083c 100644
--- a/common/entry.s2.c
+++ b/common/entry.s2.c
@@ -21,7 +21,9 @@
 #include <pxe/pxe.h>
 #include <pxe/tftp.h>
 #include <drivers/disk.h>
-#include <sys/idt.h>
+#if defined (__x86_64__) || defined (__i386__)
+#  include <sys/idt.h>
+#endif
 #include <sys/cpu.h>
 
 struct volume *boot_volume;
diff --git a/common/sys/idt.h b/common/sys/idt.h
index e9c2a074..d3a74ad2 100644
--- a/common/sys/idt.h
+++ b/common/sys/idt.h
@@ -1,8 +1,6 @@
 #ifndef SYS__IDT_H__
 #define SYS__IDT_H__
 
-#if defined (__x86_64__) || defined (__i386__)
-
 #include <stdint.h>
 #include <stddef.h>
 
@@ -60,5 +58,3 @@ void idt_register_isr(size_t vec, void *handler, uint8_t type);
 void flush_irqs(void);
 
 #endif
-
-#endif