src/config/timer.h

#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 */
[timer] Formalise the timer API 2008-10-12 19:56:52 +01:00			`#ifndef CONFIG_TIMER_H`
			`#define CONFIG_TIMER_H`

			`/** @file`
			`*`
			`* Timer configuration.`
			`*`
			`*/`

[legal] Add a selection of FILE_LICENCE declarations 2009-05-01 15:41:06 +01:00			`FILE_LICENCE ( GPL2_OR_LATER );`

[timer] Formalise the timer API 2008-10-12 19:56:52 +01:00			`#include <config/defaults.h>`

			`//#undef TIMER_PCBIOS`
			`//#define TIMER_RDTSC`

[build] Add support for local configuration files 2010-03-22 23:19:00 +01:00			`#include <config/local/timer.h>`

[timer] Formalise the timer API 2008-10-12 19:56:52 +01:00			`#endif /* CONFIG_TIMER_H */`