40a41,42
> #include "dev/arm/timer_cpulocal.hh"
>
46d47
< #include "dev/arm/timer_cpulocal.hh"