diff options
| -rw-r--r-- | toplevel/ide_slave.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 88674545ff..fc0f4f22aa 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -346,7 +346,11 @@ let eval_call xml_oc log c = in Serialize.abstract_eval_call handler c -(** Message dispatching. *) +(** Message dispatching. + Since coqtop -ideslave -coq-slaves on starts 1 thread per slave, and each + thread forwards feedback messages from the slave to the GUI on the same + xml channel, we need mutual exclusion. The mutex should be per-channel, but + here we only use 1 channel. *) let print_xml = let m = Mutex.create () in fun oc xml -> |