button_event     2225 dev/wscons/wsdisplay.c 				button_event(mouse_event.value,
button_event     2228 dev/wscons/wsdisplay.c 				button_event(mouse_event.value, 0);
button_event       46 dev/wscons/wsmoused.h void button_event(int, int);