=== modified file 'boot/arch/arm32/src/main.c'
--- boot/arch/arm32/src/main.c	2013-08-03 22:31:18 +0000
+++ boot/arch/arm32/src/main.c	2013-09-28 20:21:21 +0000
@@ -128,6 +128,9 @@
 	}
 	
 	printf(".\n");
+
+	/* Flush PT too. We need this if we disable caches later */
+	clean_dcache_poc(boot_pt, PTL0_ENTRIES * PTL0_ENTRY_SIZE);
 	
 	printf("Booting the kernel...\n");
 	jump_to_kernel((void *) PA2KA(BOOT_OFFSET), &bootinfo);

=== modified file 'kernel/arch/arm32/include/arch/mm/page_armv6.h'
--- kernel/arch/arm32/include/arch/mm/page_armv6.h	2013-08-08 20:59:02 +0000
+++ kernel/arch/arm32/include/arch/mm/page_armv6.h	2013-09-28 20:21:55 +0000
@@ -257,7 +257,7 @@
 
 	if (flags & PAGE_CACHEABLE) {
 		/*
-		 * Write-through, no write-allocate memory, see ch. B3.8.2
+		 * Write-through, write-allocate memory, see ch. B3.8.2
 		 * (p. B3-1358) of ARM Architecture reference manual.
 		 * Make sure the memory type is correct, and in sync with:
 		 * init_boot_pt (boot/arch/arm32/src/mm.c)