diff options
| author | Gaëtan Gilbert | 2019-05-04 15:49:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-10 09:47:18 +0200 |
| commit | c12c4a01e46aacb97ea3d34047a10d17630baba4 (patch) | |
| tree | d8f7f85a9ea2013453cd2b800d86fb28727aa331 /dev/ci | |
| parent | f913913a6a1b1e01d154d0c9af3b3807459b0b9f (diff) | |
CI: run coqchk without -silent
Since it's in its own job it won't pollute the log, and that way if
some issue happens it will be easier to tell what's going on.
I split the find and coqchk commands again as it's a bit confusing to
parenthesize the pipe and `|| touch` otherwise.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions