aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
diff options
context:
space:
mode:
authorEnrico Tassi2019-01-21 13:46:31 +0100
committerEnrico Tassi2019-01-22 18:03:18 +0100
commit816d8e6723c7272f2df0ff9e614f8a0fe19f66c9 (patch)
tree08547fb1a9ef780d2e7b56e99de17db3866f7b89 /configure.ml
parent05e2222e04323d11429d659b415750cf40e2babd (diff)
[thread] protect threads against sigalrm
This makes the implementation of Timeout on unix more reliable since only the main thread will receive the signal for timeout.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions