diff options
| author | Jason Gross | 2018-08-23 20:53:41 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-24 10:02:28 -0400 |
| commit | 6e65164d1a02438ea48e52229a85f8e79b6e09fb (patch) | |
| tree | 2ca4e192e4756e2475045942cb04d904d95a5ef4 /Makefile.ci | |
| parent | 05d13bf516a75da38bacbb62608528f8dceb34fd (diff) | |
Split up fiat-crypto CI into two targets
There is the new pipeline, and the old pipeline. Most of what they
share in common is the (very large) library of lemmas about `Z`.
As per the discussion in
https://github.com/coq/coq/pull/8064#issuecomment-413474176 through
https://github.com/coq/coq/pull/8064#issuecomment-413793143
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 \ |