/* cache_bit must be either CR_I or CR_C */
static void cache_enable(uint32_t cache_bit)
{
uint32_t reg;
/* The data cache is not active unless the mmu is enabled too */
/* cache_bit must be either CR_I or CR_C */
static void cache_enable(uint32_t cache_bit)
{
uint32_t reg;
/* The data cache is not active unless the mmu is enabled too */