diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-12 22:21:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-12 22:21:31 +0200 |
| commit | 582fab072375924ce380148c8a92dbc2b4ec30cc (patch) | |
| tree | 28faf805d7484ddde84857da3aebb7f4ed5cb524 /dev/ci/ci-iris-coq.sh | |
| parent | 007ab31b4d1b9457d2758a614aed5a49dee53b62 (diff) | |
| parent | 209ff6ae4367b8c96b59bc318f4791dcb2251c14 (diff) | |
Merge PR#510: Correctly identify [Time Defined.] as a defined
Diffstat (limited to 'dev/ci/ci-iris-coq.sh')
0 files changed, 0 insertions, 0 deletions