diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-13 11:33:48 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-13 11:33:48 +0100 |
| commit | ecacc9af6100f76e95acc24e777026bfc9c4d921 (patch) | |
| tree | 4c319de83cb07833fb253b2c3cd68d8a882c639b /checker/modops.mli | |
| parent | e2135c2f5fd8846c30d8099eed523fe06202b614 (diff) | |
| parent | fd5c5da475baea11d7ee2e1c2e965d7faeed3f33 (diff) | |
Merge PR#456: Proposing improvement to the CI targets for local use
Diffstat (limited to 'checker/modops.mli')
0 files changed, 0 insertions, 0 deletions