diff options
| author | Maxime Dénès | 2017-09-11 11:10:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-11 11:10:16 +0200 |
| commit | 4882288ba34ad0c47f950e733ae353a1b881df77 (patch) | |
| tree | ceb7f4578be65b102b3db97750ca42bfff7b9861 /API/API.mli | |
| parent | 550309f90cfd1786cdc9a6ab093992eecac23fd4 (diff) | |
| parent | b4958163084177157b416aaea2bde9d26ec2332b (diff) | |
Merge PR #1032: Make our CI policy clearer and more explicit
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions