+ /* Check whether the size of the window has changed, so that
+ the output drivers can adjust their settings as needed. We
+ only do this for the first line of a command, as it's
+ possible that the output drivers are actually in use
+ afterward, and we don't want to confuse them in the middle
+ of output. */
+ if (style == PROMPT_FIRST)
+ terminal_check_size ();
+
+ return !eof;
+}