Remove "killing process <pid>" messages

They convey no useful information.
2017-03-16 10:52:28 +01:00
parent 43f158bb08
commit 0ec7f47b00
4 changed files with 6 additions and 11 deletions
@@ -332,11 +332,7 @@ RunPager::~RunPager()
            pid.wait();
        }
    } catch (...) {
-        try {
-            pid.kill(true);
-        } catch (...) {
-            ignoreException();
-        }
+        ignoreException();
    }
 }