/* add_virt_timer - add an oneshot virtual CPU timer  */
void add_virt_timer(void *new)
/* add_virt_timer - add an oneshot virtual CPU timer  */
void add_virt_timer(void *new)
{
	struct vtimer_list *timer;
	timer = (struct vtimer_list *)new;
	prepare_vtimer(timer);
	timer->interval = 0;
	internal_add_vtimer(timer);
}