diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-25 12:40:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 18:55:55 +0100 |
| commit | 012e35b2d05b52dbf43dc1e26c8db550c859af03 (patch) | |
| tree | 3ae1fcb1db042f0f7581c247aaa627e0bb0c3fc1 /plugins/extraction/table.ml | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
[stm] [doc] Add some documentation to AsyncTaskQueue API
As a bonus we remove some trailing whitespace, and implement a couple
of hints suggested in the discussion.
Diffstat (limited to 'plugins/extraction/table.ml')
0 files changed, 0 insertions, 0 deletions