diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-07 11:43:37 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-07 11:43:37 +0200 |
| commit | cb2d69efa4d012a6828077675aba1d2a51d710ef (patch) | |
| tree | dfb3ce309af364daa9aa60d58e4a89936b866f4f /vernac/obligations.mli | |
| parent | 70333c957d42d3da208f442d8e7bed7133b57e5c (diff) | |
Trying to properly propagate errors in Windows CI script.
Diffstat (limited to 'vernac/obligations.mli')
0 files changed, 0 insertions, 0 deletions