| #ifndef CONFIG_TIMER_H | |
| #define CONFIG_TIMER_H | |
| /** @file | |
| * | |
| * Timer configuration. | |
| * | |
| */ | |
| FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL ); | |
| FILE_SECBOOT ( PERMITTED ); | |
| #include <config/defaults.h> | |
| //#undef TIMER_PCBIOS | |
| //#define TIMER_RDTSC | |
| #include <config/local/timer.h> | |
| #endif /* CONFIG_TIMER_H */ |