diff options
| author | Enrico Tassi | 2019-01-21 13:46:31 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-22 18:03:18 +0100 |
| commit | 816d8e6723c7272f2df0ff9e614f8a0fe19f66c9 (patch) | |
| tree | 08547fb1a9ef780d2e7b56e99de17db3866f7b89 /stm/spawned.ml | |
| parent | 05e2222e04323d11429d659b415750cf40e2babd (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 'stm/spawned.ml')
| -rw-r--r-- | stm/spawned.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/spawned.ml b/stm/spawned.ml index a5d6ea96f9..bd772d825d 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -38,7 +38,7 @@ let controller h pr pw = prerr_endline ("control channel broken: " ^ Printexc.to_string e); exit 1 in loop () in - ignore(Thread.create main ()) + ignore(CThread.create main ()) let main_channel = ref None let control_channel = ref None |