diff --git a/src/kernel/core/arch/ppc/arch_int.c b/src/kernel/core/arch/ppc/arch_int.c
index c25716fda0..5c7d45b00b 100755
--- a/src/kernel/core/arch/ppc/arch_int.c
+++ b/src/kernel/core/arch/ppc/arch_int.c
@@ -33,6 +33,9 @@ arch_int_disable_io_interrupt(int irq)
 }
 
 
+/* arch_int_*_interrupts() and friends are in arch_asm.S */
+
+
 static void 
 print_iframe(struct iframe *frame)
 {