#ifndef __GENERIC_ARMCM_TIMER_H
#define __GENERIC_ARMCM_TIMER_H
#include <stdint.h> // uint32_t
void udelay(uint32_t usecs);
#endif // armcm_timer.h