diff options
| author | Gaëtan Gilbert | 2018-08-27 19:57:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-08-27 19:57:54 +0200 |
| commit | 5e2eedb3f9068a87eda0d7e08c82127ddef224fb (patch) | |
| tree | 9480dd7a94dee5e13528d06bd85d717f89866d54 /Makefile.ci | |
| parent | bce734bfb2a118dbb487e5b88eba524ca14d2078 (diff) | |
| parent | 6e65164d1a02438ea48e52229a85f8e79b6e09fb (diff) | |
Merge PR #8312: Split up fiat-crypto CI into two targets
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci index fce16906c4..306471d1d0 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -22,6 +22,7 @@ CI_TARGETS=ci-bedrock2 \ ci-equations \ ci-fcsl-pcm \ ci-fiat-crypto \ + ci-fiat-crypto-legacy \ ci-fiat-parsers \ ci-flocq \ ci-formal-topology \ |