/* Adjust the speed of the clock source by a multiplicative factor  */
void native_rtc_adjust_clock(double clock_correction)
/* Adjust the speed of the clock source by a multiplicative factor  */
void native_rtc_adjust_clock(double clock_correction)
{
	hwtimer_adjust_rt_ratio(clock_correction);
}