diff options
| author | Maxime Dénès | 2017-08-16 09:39:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:39:06 +0200 |
| commit | 335f219436fd1106884a0f135826a53f01801728 (patch) | |
| tree | 6a9cf62e450a6962a50dbb3262386fce6529f28e /API/API.mli | |
| parent | 48e2ccee3614503dfbc18edf5ae8f1f230927d1a (diff) | |
| parent | 479ba134a1af676b7b8f3f60c3709761fd0d0b51 (diff) | |
Merge PR #943: Reference Manual: minor wording improvements
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions