aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-12-25 15:51:07 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-12-25 16:05:27 +0100
commit0e326def6194606d0f1e21daeb45f32e1a061c8f (patch)
treeb6343d4b7601a7503c1f90e265cd852160304606 /theories/Program
parent90ed6636dea41486ddf2cc0daead83f9f0788163 (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 'theories/Program')
0 files changed, 0 insertions, 0 deletions