timer.h

Go to the documentation of this file.
00001 #ifndef CONFIG_TIMER_H
00002 #define CONFIG_TIMER_H
00003 
00004 /** @file
00005  *
00006  * Timer configuration.
00007  *
00008  */
00009 
00010 FILE_LICENCE ( GPL2_OR_LATER );
00011 
00012 #include <config/defaults.h>
00013 
00014 //#undef                TIMER_PCBIOS
00015 //#define               TIMER_RDTSC
00016 
00017 #include <config/local/timer.h>
00018 
00019 #endif /* CONFIG_TIMER_H */