diff --git a/boot/device/crt0.c b/boot/device/crt0.c
index 440262eb2..8ad3b0119 100644
--- a/boot/device/crt0.c
+++ b/boot/device/crt0.c
@@ -13,6 +13,7 @@ extern char _bss_section_end_ram;
 void enable_fpu() {
   // http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0553a/BABDBFBJ.html
   CPACR |= (0xF << 20); // Set the bits 20-23 to enable CP10 and CP11 coprocessors
+  // FIXME: The pipeline should be flushed at this point
 }
 
 void abort() {