diff options
-rw-r--r-- | src/libmain/shared.cc | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/libmain/shared.cc b/src/libmain/shared.cc index 8d06455fa739..7b50bfa9bb32 100644 --- a/src/libmain/shared.cc +++ b/src/libmain/shared.cc @@ -328,10 +328,14 @@ RunPager::RunPager() RunPager::~RunPager() { - if (pid != -1) { - std::cout.flush(); - close(STDOUT_FILENO); - pid.wait(true); + try { + if (pid != -1) { + std::cout.flush(); + close(STDOUT_FILENO); + pid.wait(true); + } + } catch (...) { + ignoreException(); } } |