diff options
| author | Arthur Azevedo de Amorim | 2021-03-09 09:57:19 -0500 |
|---|---|---|
| committer | Arthur Azevedo de Amorim | 2021-03-11 14:29:10 -0500 |
| commit | b1dec36c75d883f84babe534be3a47d44633f4f7 (patch) | |
| tree | 9e3e386e890df596ddd79f55a16e84d74192fbef /Makefile.ci | |
| parent | b55216ab3509f48e45aac035f1b799529d068f51 (diff) | |
Add deriving lib to CI.
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci index d549ed1b39..c589c95258 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -24,6 +24,7 @@ CI_TARGETS= \ ci-coq_performance_tests \ ci-coq_tools \ ci-coqprime \ + ci-deriving \ ci-elpi \ ci-engine_bench \ ci-ext_lib \ @@ -74,6 +75,7 @@ ci-color: ci-bignums ci-coqprime: ci-bignums ci-coquelicot: ci-mathcomp +ci-deriving: ci-mathcomp ci-math_classes: ci-bignums ci-corn: ci-math_classes |