Index: kernel/arch/arm32/include/arch/mm/page.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page.h	(revision 0c40fd50243688f325f369871c3ae638910d5aec)
+++ kernel/arch/arm32/include/arch/mm/page.h	(revision ae5fb7c8167b12c7be26bb5b4830aa37837e6eba)
@@ -146,5 +146,8 @@
  *
  * Page tables are always in cacheable memory.
- * Make sure the memory type is correct.
+ * Make sure the memory type is correct, and in sync with:
+ * init_boot_pt (boot/arch/arm32/src/mm.c)
+ * init_ptl0_section (boot/arch/arm32/src/mm.c)
+ * set_pt_level1_flags (kernel/arch/arm32/include/arch/mm/page_armv6.h)
  */
 NO_TRACE static inline void set_ptl0_addr(pte_t *pt)
Index: kernel/arch/arm32/include/arch/mm/page_armv6.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision 0c40fd50243688f325f369871c3ae638910d5aec)
+++ kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision ae5fb7c8167b12c7be26bb5b4830aa37837e6eba)
@@ -260,4 +260,8 @@
 		 * Write-through, no 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)
+		 * init_ptl0_section (boot/arch/arm32/src/mm.c)
+		 * set_ptl0_addr (kernel/arch/arm32/include/arch/mm/page.h)
 		 */
 		//TODO: Use writeback, write-allocate caches