tag	line	file	source code
do_keyboard_interrupt	60	drivers/char/keyboard.c	extern void do_keyboard_interrupt(void);
do_keyboard_interrupt	817	drivers/char/keyboard.c	do_keyboard_interrupt();