diff options
| author | Emilio Jesus Gallego Arias | 2019-05-10 13:31:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-10 13:31:41 +0200 |
| commit | c659b96eaa7bb5e401786546bb293a31e5f3c3d4 (patch) | |
| tree | d8f7f85a9ea2013453cd2b800d86fb28727aa331 /dev | |
| parent | f913913a6a1b1e01d154d0c9af3b3807459b0b9f (diff) | |
| parent | c12c4a01e46aacb97ea3d34047a10d17630baba4 (diff) | |
Merge PR #10065: CI: run coqchk without -silent
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions