From 0ec7f47b00659cf043eb7fbe72385a08f7e9f8e2 Mon Sep 17 00:00:00 2001
From: Eelco Dolstra <edolstra@gmail.com>
Date: Thu, 16 Mar 2017 10:52:28 +0100
Subject: Remove "killing process <pid>" messages

They convey no useful information.
---
 src/libmain/shared.cc | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'src/libmain/shared.cc')

diff --git a/src/libmain/shared.cc b/src/libmain/shared.cc
index 326202d295fb..a720afd6cdd4 100644
--- a/src/libmain/shared.cc
+++ b/src/libmain/shared.cc
@@ -332,11 +332,7 @@ RunPager::~RunPager()
             pid.wait();
         }
     } catch (...) {
-        try {
-            pid.kill(true);
-        } catch (...) {
-            ignoreException();
-        }
+        ignoreException();
     }
 }
 
-- 
cgit 1.4.1