tag	line	file	source code
timer_interrupt	45	kernel/sched.c	extern int timer_interrupt(void);
timer_interrupt	411	kernel/sched.c	set_intr_gate(0x20,&timer_interrupt);