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