diff options
author | Eelco Dolstra <edolstra@gmail.com> | 2017-03-16T09·52+0100 |
---|---|---|
committer | Eelco Dolstra <edolstra@gmail.com> | 2017-03-16T09·52+0100 |
commit | 0ec7f47b00659cf043eb7fbe72385a08f7e9f8e2 (patch) | |
tree | 820dd15bf3c739616b177e7d8279997622e74822 /src/libmain/shared.cc | |
parent | 43f158bb0885c2eb9180ef7ab24034b1b9353e8b (diff) |
Remove "killing process <pid>" messages
They convey no useful information.
Diffstat (limited to 'src/libmain/shared.cc')
-rw-r--r-- | src/libmain/shared.cc | 6 |
1 files changed, 1 insertions, 5 deletions
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(); } } |