Index: kernel/arch/ppc32/src/interrupt.c
===================================================================
--- kernel/arch/ppc32/src/interrupt.c	(revision 6c3106f2799b7a9663b846f3973d4b21e90bfb2a)
+++ kernel/arch/ppc32/src/interrupt.c	(revision 622f40971c4de54afef879c8d7d1bc1e522942ee)
@@ -42,4 +42,5 @@
 #include <arch/drivers/pic.h>
 #include <arch/mm/tlb.h>
+#include <arch/mm/pht.h>
 #include <print.h>