diff options
| author | Maxime Dénès | 2017-12-05 09:58:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-05 09:58:13 +0100 |
| commit | 3e71e1961aae51b71a16ef0afe2a4473060f24ec (patch) | |
| tree | ba671a95bb808a2e909a972e07905aea13573000 /API/API.mli | |
| parent | 2ae7674c6788742c021988ac02caabceec958957 (diff) | |
| parent | 500d33872a4f280a640bfc3ef02752f9e68643c7 (diff) | |
Merge PR #6300: Clarify operation of sequences, fixes #6095
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions