mirror of https://github.com/CGAL/cgal
Once the timeout is reach, kill -KILL the whole process group, instead of
just the group leader (in case a process catches SIGHUP).
This commit is contained in:
parent
5d97e6dc26
commit
03c0ce5e68
|
|
@ -71,7 +71,7 @@ wait_for_process()
|
|||
kill -HUP $pid
|
||||
sleep 10
|
||||
# If SIGHUP was not enough, SIGKILL will finish the job, 10s after.
|
||||
kill -KILL $pid
|
||||
kill -KILL -$pid
|
||||
fi
|
||||
return 1
|
||||
fi
|
||||
|
|
|
|||
Loading…
Reference in New Issue