set_fullscreen_state 4450 src/pgtkterm.c       set_fullscreen_state (f);
set_fullscreen_state 5483 src/pgtkterm.c 	set_fullscreen_state (f);