x_set_gtk_user_time 20048 src/xterm.c    	x_set_gtk_user_time (f, event->xkey.time);
x_set_gtk_user_time 23913 src/xterm.c    		x_set_gtk_user_time (f, xev->time);
x_set_gtk_user_time 28565 src/xterm.c    	      x_set_gtk_user_time (f, time);