#include <asm/leds.h>
#include <asm/thread_info.h>
+#include <asm/sched_clock.h>
#include <asm/stacktrace.h>
#include <asm/mach/arch.h>
#include <asm/mach/time.h>
{
system_timer = machine_desc->timer;
system_timer->init();
+#ifdef CONFIG_HAVE_SCHED_CLOCK
+ sched_clock_postinit();
+#endif
}