diff options
| author | Gaëtan Gilbert | 2019-03-11 13:52:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-11 13:52:21 +0100 |
| commit | 0e2bb26240b785d4ca618cfbc042b13c613fa78f (patch) | |
| tree | b2d558d2bf34f0bc731062a71b46c9f7f3e43420 /plugins | |
| parent | 74534f84a782f5de740c52cb97b3ca3a02eb6aa2 (diff) | |
Don't coqchk the test suite prerequisites
This causes the makefile to break due to dependencies when it fails,
and it's not worth adding a whole mess of code to catch the failure
for these files.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions