diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-25 15:51:07 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-25 16:05:27 +0100 |
commit | 0e326def6194606d0f1e21daeb45f32e1a061c8f (patch) | |
tree | b6343d4b7601a7503c1f90e265cd852160304606 /library/declaremods.ml | |
parent | 90ed6636dea41486ddf2cc0daead83f9f0788163 (diff) |
Inlining Spawn.kill_if in the one place were it was actually used, thus
removing the need of thread creation in the interface.
Diffstat (limited to 'library/declaremods.ml')
0 files changed, 0 insertions, 0 deletions