gui_update_window_end 3778 src/dispextern.h extern void gui_update_window_end (struct window *, bool, bool);
gui_update_window_end 3866 src/dispnew.c        gui_update_window_end (w, !paused_p, mouse_face_overwritten_p);
gui_update_window_end 21213 src/xdisp.c    	      gui_update_window_end (w, false, false);
gui_update_window_end 21381 src/xdisp.c    	  gui_update_window_end (w, false, false);
gui_update_window_end 22364 src/xdisp.c    	  gui_update_window_end (w, false, false);