src/config/timer.h

   1 #ifndef CONFIG_TIMER_H
   2 #define CONFIG_TIMER_H
   3
   4 /** @file
   5  *
   6  * Timer configuration.
   7  *
   8  */
   9
  10 FILE_LICENCE ( GPL2_OR_LATER );
  11
  12 #include <config/defaults.h>
  13
  14 //#undef                TIMER_PCBIOS
  15 //#define               TIMER_RDTSC
  16
  17 #include <config/local/timer.h>
  18
  19 #endif /* CONFIG_TIMER_H */