--- a/src/pager.cc	Thu Dec 15 01:18:38 1994 +0000
+++ b/src/pager.cc	Thu Dec 15 03:59:06 1994 +0000
@@ -119,14 +119,16 @@
 void
 flush_output_to_pager (void)
 {
-  *pager_buf << ends;
+ // Extract message from buffer, then delete the buffer so that any
+ // new messages get sent separately.
 
+  *pager_buf << ends;
   char *message = pager_buf->str ();
+  initialize_pager ();
 
   if (! message || ! *message)
     {
       delete [] message;
-      initialize_pager ();
       return;
     }
 
@@ -143,19 +145,16 @@
 	  if (pager_stream)
 	    {
 	      pager_stream << message;
+	      delete [] message;
 	      pager_stream.flush ();
-
-	      delete [] message;
-	      initialize_pager ();
 	      return;
 	    }
 	}
     }
 
   cout << message;
+  delete [] message;
   cout.flush ();
-  delete [] message;
-  initialize_pager ();
 }
 
 static void