diff --git a/src/system/boot/platform/raspberrypi_arm/mmu.cpp b/src/system/boot/platform/raspberrypi_arm/mmu.cpp
index 1ecc57411d..f01bacc40a 100644
--- a/src/system/boot/platform/raspberrypi_arm/mmu.cpp
+++ b/src/system/boot/platform/raspberrypi_arm/mmu.cpp
@@ -241,17 +241,22 @@ mmu_write_DACR(uint32 value)
 static uint32 *
 get_next_page_table(uint32 type)
 {
-	TRACE("%s: sNextPageTableAddress %p, kPageTableRegionEnd %p, type  0x%lx\n",
-		__func__, sNextPageTableAddress, kPageTableRegionEnd, type);
+	TRACE("%s: sNextPageTableAddress %p, kPageTableRegionEnd %p, "
+		"type 0x" B_PRIX32 "\n", __func__, sNextPageTableAddress,
+		kPageTableRegionEnd, type);
 
 	size_t size = 0;
 	switch(type) {
 		case MMU_L1_TYPE_COARSE:
+		default:
 			size = 1024;
-		break;
+			break;
 		case MMU_L1_TYPE_FINE:
 			size = 4096;
-		break;
+			break;
+		case MMU_L1_TYPE_SECTION:
+			size = 16384;
+			break;
 	}
 
 	addr_t address = sNextPageTableAddress;
diff --git a/src/system/boot/platform/u-boot/mmu.cpp b/src/system/boot/platform/u-boot/mmu.cpp
index 0057213e8c..60891dcfdd 100644
--- a/src/system/boot/platform/u-boot/mmu.cpp
+++ b/src/system/boot/platform/u-boot/mmu.cpp
@@ -253,15 +253,21 @@ static uint32 *
 get_next_page_table(uint32 type)
 {
 	TRACE(("get_next_page_table, sNextPageTableAddress %p, kPageTableRegionEnd "
-		"%p, type  0x%lx\n", sNextPageTableAddress, kPageTableRegionEnd, type));
+		"%p, type 0x" B_PRIX32 "\n", sNextPageTableAddress,
+		kPageTableRegionEnd, type));
+
 	size_t size = 0;
 	switch(type) {
 		case MMU_L1_TYPE_COARSE:
+		default:
 			size = 1024;
-		break;
+			break;
 		case MMU_L1_TYPE_FINE:
 			size = 4096;
-		break;
+			break;
+		case MMU_L1_TYPE_SECTION:
+			size = 16384;
+			break;
 	}
 
 	addr_t address = sNextPageTableAddress;