diff options
| author | Maxime Dénès | 2016-09-01 14:22:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-01 14:23:37 +0200 |
| commit | 5ea872c80cc8b9d2845629cc75369f061e3bad05 (patch) | |
| tree | 5c6183c776812e100a6694094ec9631e38fbc980 /stm/asyncTaskQueue.ml | |
| parent | 5776f7d2b4753b89efa095a0f6774dac702fdfbd (diff) | |
More efficient data structure to check if a native file is loaded.
Spotted by PMP.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions