diff options
| author | Pierre Roux | 2020-11-14 12:25:10 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-11-20 19:08:08 +0100 |
| commit | 787c4583d685e4059c2a08cdb9fe0bbfa99e255e (patch) | |
| tree | b6a66af14d064482f4134e1cd177fb9a5c4d8fca /dev/ci/ci-compcert.sh | |
| parent | 146415fb624c182493d46413d738a3c2c3f47e02 (diff) | |
[CI] Deactivate native-compiler for a few tests that fail with it
Diffstat (limited to 'dev/ci/ci-compcert.sh')
0 files changed, 0 insertions, 0 deletions