ensure_echo_area_buffers 12390 src/xdisp.c      ensure_echo_area_buffers ();
ensure_echo_area_buffers 12555 src/xdisp.c      ensure_echo_area_buffers ();