Index: kernel/arch/arm32/include/arch/cache.h
===================================================================
--- kernel/arch/arm32/include/arch/cache.h	(revision ee6f4342058a8205c52ba1e31e063a17c0cf6f18)
+++ kernel/arch/arm32/include/arch/cache.h	(revision e8d3c6f55fdb9a5a1e2e4d95612cb04c4ea82652)
@@ -39,10 +39,10 @@
 #include <typedefs.h>
 
-unsigned dcache_levels(void);
+extern unsigned dcache_levels(void);
 
-void dcache_flush(void);
-void dcache_flush_invalidate(void);
-void cpu_dcache_flush(void);
-void cpu_dcache_flush_invalidate(void);
+extern void dcache_flush(void);
+extern void dcache_flush_invalidate(void);
+extern void cpu_dcache_flush(void);
+extern void cpu_dcache_flush_invalidate(void);
 extern void icache_invalidate(void);
 extern void dcache_invalidate(void);
@@ -50,5 +50,5 @@
 
 #endif
+
 /** @}
  */
-