ensure_echo_area_buffers 12398 src/xdisp.c      ensure_echo_area_buffers ();
ensure_echo_area_buffers 12563 src/xdisp.c      ensure_echo_area_buffers ();