aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-06-29 17:03:39 +0200
committerEmilio Jesus Gallego Arias2020-07-08 15:12:46 +0200
commit22e2ab01dd9fe4d6b6afb6d1bb171cbf11db4a3f (patch)
tree73c90f7c2d1807950d55b449eb8858459ef58aed /dev/ci
parent4413a1fb74fc2fd33176e5983a9977f9e28218d9 (diff)
[ci] Overlay for metacoq and rewriter
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh14
1 files changed, 10 insertions, 4 deletions
diff --git a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
index 232ca2bf0d..72ec55a37c 100644
--- a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
+++ b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh
@@ -1,12 +1,18 @@
if [ "$CI_PULL_REQUEST" = "11836" ] || [ "$CI_BRANCH" = "obligations+functional" ]; then
- equations_CI_REF=obligations+functional
- equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+ mtac2_CI_REF=obligations+functional
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
paramcoq_CI_REF=obligations+functional
paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
- mtac2_CI_REF=obligations+functional
- mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+ equations_CI_REF=obligations+functional
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ metacoq_CI_REF=obligations+functional
+ metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+ rewriter_CI_REF=obligations+functional
+ rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
fi