/*
*/
-#include <stat_time.h>
#include <machine_timer_routines.h>
#include <mach/kern_return.h>
#include <kern/sched_prim.h>
#include <kern/timer.h>
+int precise_user_kernel_time = 1;
+
/*
* timer_init initializes a timer.
*/
timer_init(
timer_t timer)
{
-#if !STAT_TIME
timer->tstamp = 0;
-#endif /* STAT_TIME */
#if defined(__LP64__)
timer->all_bits = 0;
#else
#endif /* defined(__LP64__) */
}
-#if !STAT_TIME
-
void
timer_start(
timer_t timer,
}
#endif /* MACHINE_TIMER_ROUTINES */
-
-#endif /* STAT_TIME */