# HG changeset patch
# User jwe
# Date 787471097 0
# Node ID d2dd114ba5dd37c3310035d784e9a4e3cd925fc6
# Parent  afb9c5c14ed366317e26939cef31dfaada99558d
[project @ 1994-12-15 05:58:17 by jwe]

diff -r afb9c5c14ed3 -r d2dd114ba5dd src/pager.cc
--- a/src/pager.cc	Thu Dec 15 04:03:35 1994 +0000
+++ b/src/pager.cc	Thu Dec 15 05:58:17 1994 +0000
@@ -25,6 +25,7 @@
 #include "config.h"
 #endif
 
+#include <signal.h>
 #include <iostream.h>
 #include <strstream.h>
 #include <fstream.h>
@@ -32,6 +33,7 @@
 
 #include "procstream.h"
 
+#include "sighandlers.h"
 #include "user-prefs.h"
 #include "oct-obj.h"
 #include "error.h"
@@ -144,9 +146,15 @@
 	  oprocstream pager_stream (pgr);
 	  if (pager_stream)
 	    {
+	      volatile sig_handler *old_sigint_handler;
+	      old_sigint_handler = signal (SIGINT, SIG_IGN);
+
 	      pager_stream << message;
 	      delete [] message;
 	      pager_stream.flush ();
+
+	      signal (SIGINT, old_sigint_handler);
+
 	      return;
 	    }
 	}