diff options
| author | Vincent Laporte | 2018-10-04 15:10:10 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-12-10 15:03:12 +0000 |
| commit | 21bac03b0997cd79ddf6a8a9b31ee4d8ee63f50a (patch) | |
| tree | fcc60d263f1ad6f6ecc7aaa469eb56d8ed4dff8d /dev/ci/ci-plugin_tutorial.sh | |
| parent | 10b07a187522b74bbcc9355d3ff9c4153f300706 (diff) | |
[test-suite] Run `coqchk` on most test cases
Diffstat (limited to 'dev/ci/ci-plugin_tutorial.sh')
0 files changed, 0 insertions, 0 deletions