diff options
| author | Maxime Dénès | 2017-06-14 18:12:03 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 18:12:03 +0200 |
| commit | 42843f73e30eae57684269479193389242a0c1b1 (patch) | |
| tree | 8a09a3452cd4d4afe91dd31cecd7899256bd0dfc /API/API.mli | |
| parent | e9ad450304fca010812a04e8417b111f4910156a (diff) | |
| parent | b5e90d92fc52e568f1ed6e65a4b611bdab80e8f5 (diff) | |
Merge PR#739: completing a sentence in a comment
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions