xg_end_scroll_callback 3997 src/pgtkterm.c 			G_CALLBACK (xg_end_scroll_callback), scroll_bar_name);
xg_end_scroll_callback 4009 src/pgtkterm.c 				   G_CALLBACK (xg_end_scroll_callback),
xg_end_scroll_callback 15340 src/xterm.c    xg_end_scroll_callback (GtkWidget *widget,
xg_end_scroll_callback 15508 src/xterm.c                            G_CALLBACK (xg_end_scroll_callback),
xg_end_scroll_callback 15520 src/xterm.c    				   G_CALLBACK (xg_end_scroll_callback),