|
@@ -937,7 +937,6 @@ void __init time_init(void)
|
|
vxtime.mode = VXTIME_TSC;
|
|
vxtime.mode = VXTIME_TSC;
|
|
vxtime.quot = (1000000L << 32) / vxtime_hz;
|
|
vxtime.quot = (1000000L << 32) / vxtime_hz;
|
|
vxtime.tsc_quot = (1000L << 32) / cpu_khz;
|
|
vxtime.tsc_quot = (1000L << 32) / cpu_khz;
|
|
- vxtime.hz = vxtime_hz;
|
|
|
|
rdtscll_sync(&vxtime.last_tsc);
|
|
rdtscll_sync(&vxtime.last_tsc);
|
|
setup_irq(0, &irq0);
|
|
setup_irq(0, &irq0);
|
|
|
|
|