diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-05 18:39:06 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-08 09:51:13 +0200 |
| commit | 188ab7f76459ab46e0ea139da8b4331d958c7102 (patch) | |
| tree | 0f2e7de5326e7f53d9a4a422b4b722317ffbf6d4 /stm/spawned.mli | |
| parent | f7e9e6428842dd80549a0dcd20bf872c2dd7fa8c (diff) | |
Spawn: use each socket exclusively for writing or reading
According to http://caml.inria.fr/mantis/view.php?id=5325
you can't use the same socket for both writing and reading.
The result is lockups (may be fixed in 4.03).
Diffstat (limited to 'stm/spawned.mli')
| -rw-r--r-- | stm/spawned.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/spawned.mli b/stm/spawned.mli index d9e7baff3..d0183e081 100644 --- a/stm/spawned.mli +++ b/stm/spawned.mli @@ -8,7 +8,7 @@ (* To link this file, threads are needed *) -type chandescr = AnonPipe | Socket of string * int +type chandescr = AnonPipe | Socket of string * int * int (* Argument parsing should set these *) val main_channel : chandescr option ref |