/* Stop announcing sys ticks into the kernel. 
Disable the system ticks generation  */
void sys_clock_disable(void)
/* Stop announcing sys ticks into the kernel. 
Disable the system ticks generation  */
void sys_clock_disable(void)
{
	irq_disable(TIMER_TICK_IRQ);
	hwtimer_set_silent_ticks(INT64_MAX);
}