diff options
| author | coqbot-app[bot] | 2021-03-13 19:37:47 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-13 19:37:47 +0000 |
| commit | def498d87d9ad43e43bd8e6e70b8d8f6ae9272be (patch) | |
| tree | 97ce65edc51f8621298a7f24bfedf3b0c430cd97 /Makefile.ci | |
| parent | 953008d7cbb928ca424834bd516c7d21df769fa2 (diff) | |
| parent | b1dec36c75d883f84babe534be3a47d44633f4f7 (diff) | |
Merge PR #13917: Add deriving lib to CI.
Reviewed-by: ejgallego
Ack-by: SkySkimmer
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 |