#endif
/* "static data" needed by most of timer.c on ARM platforms */
unsigned long timer_rate_hz;
- unsigned long tbu;
- unsigned long tbl;
+ unsigned int tbu;
+ unsigned int tbl;
unsigned long lastinc;
unsigned long long timer_reset_value;
#if !(defined(CONFIG_SYS_ICACHE_OFF) && defined(CONFIG_SYS_DCACHE_OFF))