32a33,34
> #include "dev/intel_8254_timer.hh"
>
35d36
< #include "dev/intel_8254_timer.hh"