--- /dev/null
+#ifndef CONFIG_TIMER_H
+#define CONFIG_TIMER_H
+
+/** @file
+ *
+ * Timer configuration.
+ *
+ */
+
+FILE_LICENCE ( GPL2_OR_LATER );
+
+#include <config/defaults.h>
+
+//#undef TIMER_PCBIOS
+//#define TIMER_RDTSC
+
+#include <config/local/timer.h>
+
+#endif /* CONFIG_TIMER_H */