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 #include <config/defaults.h>
  11
  12 //#undef                TIMER_PCBIOS
  13 //#define               TIMER_RDTSC
  14
  15 #endif /* CONFIG_TIMER_H */