diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-22 10:23:14 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-26 14:20:52 +0100 |
| commit | ea17a2a371d0d791f439e0a4c6610819ecb6f9b6 (patch) | |
| tree | e7a91131f773efedbbcdb79d035b6c6d443b1e55 /lib/lib.mllib | |
| parent | 26b6134c3cd333d7fc78c665be5fd1394a546395 (diff) | |
Spawn: managed processes
The Spawn and Spawned modules factor the operation of spawning
a process. Both synchronous and asynchronous channels are supported.
Both threaded and glib like main loop models are supported. Still,
not all combinations are truly tested not equipped with a decent API:
only async + glib and sync + thread are, since these are the models we
use for coqide<->coqtop and coqtop<->worker respectively.
Diffstat (limited to 'lib/lib.mllib')
| -rw-r--r-- | lib/lib.mllib | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib index f641e68f0..be15eca60 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -8,6 +8,8 @@ Segmenttree Unicodetable Unicode System +Spawn +Spawned Trie Profile Explore |