# HG changeset patch
# User jwe
# Date 783795492 0
# Node ID b57450f85c07b3d59f2fc46e29449d6f699fe69f
# Parent  05428c0044cc7565551a1a2deb2d8cffb7be43c0
[project @ 1994-11-02 16:58:12 by jwe]

diff -r 05428c0044cc -r b57450f85c07 src/file-io.cc
--- a/src/file-io.cc	Wed Nov 02 16:26:12 1994 +0000
+++ b/src/file-io.cc	Wed Nov 02 16:58:12 1994 +0000
@@ -1352,7 +1352,14 @@
       if (strcmp (type, "scanf") == 0
 	  || (doing_fscanf && file.number () == 0))
 	{
+// XXX FIXME XXX -- this should probably be possible for more than
+// just stdin/stdout pairs, using a list of output streams to flush.
+// The list could be created with a function like iostream's tie().
+
+	  flush_output_to_pager ();
+
 	  string = gnu_readline ("");
+
 	  if (string && *string)
 	    maybe_save_history (string);
 	}