Index: kernel/arch/arm32/include/arch/cache.h
===================================================================
--- kernel/arch/arm32/include/arch/cache.h	(revision d4a829e15ff53d4529f6faccc7aa01dc9efccd08)
+++ kernel/arch/arm32/include/arch/cache.h	(revision 13dc048ab1b8dfe020d96582cf64de71305f3834)
@@ -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
+
 /** @}
  */
-