mouse_copy_end   2270 dev/wscons/wsdisplay.c 			mouse_copy_end();
mouse_copy_end     63 dev/wscons/wsmoused.h void mouse_copy_end(void);