aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-03-31 11:05:21 +0200
committerGaëtan Gilbert2020-03-31 11:05:21 +0200
commit29bcd98d55ccb9a90dff7fc8f254578c4d870a09 (patch)
treec87bee672d196212e4f0033804e57c00deadeef8 /dev/ci
parentc31a634b1f57028f3491b61137e53978d2653bbe (diff)
parent1320d5004b58f33c2274bfdc0629d7f513cd49c4 (diff)
Merge PR #11818: [proof] Further consolidation of the regular declaration path
Ack-by: Matafou Reviewed-by: SkySkimmer
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh15
1 files changed, 15 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
new file mode 100644
index 0000000000..e3a8eb07f3
--- /dev/null
+++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then
+
+ metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+ metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+ elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+ paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+ equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi