aboutsummaryrefslogtreecommitdiff
path: root/mod
diff options
context:
space:
mode:
authorKaren Arutyunov <karen@codesynthesis.com>2020-11-06 17:59:07 +0300
committerKaren Arutyunov <karen@codesynthesis.com>2020-11-06 17:59:07 +0300
commit069e21c82557fa45ce59e340a5aaf6ef691b89b5 (patch)
treee05b8a69f762ae654273aa596fa9021a1f0dfca6 /mod
parent6163f829355b6ceae21060eb7a33f3107477d899 (diff)
Adapt to process::kill() semantics change
Diffstat (limited to 'mod')
-rw-r--r--mod/external-handler.cxx3
1 files changed, 3 insertions, 0 deletions
diff --git a/mod/external-handler.cxx b/mod/external-handler.cxx
index 7f26680..2f58bf5 100644
--- a/mod/external-handler.cxx
+++ b/mod/external-handler.cxx
@@ -95,6 +95,8 @@ namespace brep
data_dir));
pipe.out.close ();
+ // Kill the process and wait for its completion.
+ //
auto kill = [&pr, &warn, &handler, &ref] ()
{
// We may still end up well (see below), thus this is a warning.
@@ -103,6 +105,7 @@ namespace brep
<< " execution timeout expired";
pr.kill ();
+ pr.wait ();
};
try