x_set_gtk_user_time 19673 src/xterm.c    	x_set_gtk_user_time (f, event->xkey.time);
x_set_gtk_user_time 23386 src/xterm.c    		x_set_gtk_user_time (f, xev->time);
x_set_gtk_user_time 27772 src/xterm.c    	      x_set_gtk_user_time (f, time);