diff options
| author | Enrico Tassi | 2016-09-13 09:37:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-13 12:58:07 +0200 |
| commit | 5d3718123afed16691843b5d7bcd5841b18f95ac (patch) | |
| tree | 00b1e5512d53cfb268a2ca57ca7d718b5459b21c /stm/asyncTaskQueue.ml | |
| parent | a5fb20b4ad4a56e15455ca329fbc4d03ac5fe072 (diff) | |
stm: feedback forwarding has to be atomic
I think that a better place for the mutex would be the printing routine,
but I still hope we will get rid of threads in favor of coroutines.
So I keep all mutexes in Stm.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions