diff options
| author | Gaëtan Gilbert | 2019-06-07 11:15:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-07 11:16:40 +0200 |
| commit | 135b56936e36eff23eb580c097045d2a932a19f8 (patch) | |
| tree | 688ff27d8af4e8e61780cf832ba2129b49d925c4 /doc/plugin_tutorial/tuto2/Makefile | |
| parent | 32f965d53d7e0f969af5f9c52adc5cf7bd2a97a3 (diff) | |
test suite: don't try to coqchk failed tests
Diffstat (limited to 'doc/plugin_tutorial/tuto2/Makefile')
0 files changed, 0 insertions, 0 deletions