diff --git a/src/kernel/boot/platform/bios_ia32/mmu.h b/src/kernel/boot/platform/bios_ia32/mmu.h
index 9d24f7490d..919885b411 100644
--- a/src/kernel/boot/platform/bios_ia32/mmu.h
+++ b/src/kernel/boot/platform/bios_ia32/mmu.h
@@ -14,6 +14,7 @@ extern "C" {
 #endif
 
 extern void mmu_init(void);
+extern void mmu_init_for_kernel(void);
 extern void *mmu_allocate(void *virtualAddress, size_t size);
 extern void mmu_free(void *virtualAddress, size_t size);