diff options
| author | Gaëtan Gilbert | 2021-04-06 17:24:01 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-04-06 17:24:01 +0200 |
| commit | 89c7574ce888c4f8ee619b12e2182154ffb3a24a (patch) | |
| tree | 711cd86f27eab9e9ecddacd3022d36b2711f4373 /doc/plugin_tutorial/tuto1 | |
| parent | 2360e5ba31c350f25d49fc71736282bfad9975ed (diff) | |
CI-paramcoq: Re-enable native
It's an issue in paramcoq's test suite, which doesn't respect
COQEXTRAFLAGS and so will be handled upstream
(https://github.com/coq-community/paramcoq/pull/66)
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions