--- a/src/pager.cc	Wed Feb 02 11:18:39 2000 +0000
+++ b/src/pager.cc	Wed Feb 02 11:33:32 2000 +0000
@@ -108,7 +108,7 @@
 	  // Avoid warning() or error(), since that will put us back in
 	  // the pager, which would be bad news.
 
-	  cerr << "warning: connection to external pager (pid = "
+	  std::cerr << "warning: connection to external pager (pid = "
 	       << pid << ") lost --\n"
 	       << "warning: attempting to finish pending computations...\n";
 	}
@@ -122,8 +122,8 @@
     {
       if (bypass_pager)
 	{
-	  cout.write (msg, len);
-	  cout.flush ();
+	  std::cout.write (msg, len);
+	  std::cout.flush ();
 	}
       else
 	{
@@ -178,8 +178,8 @@
 	    }
 	  else
 	    {
-	      cout.write (msg, len);
-	      cout.flush ();
+	      std::cout.write (msg, len);
+	      std::cout.flush ();
 	    }
 	}
     }