aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-02-12 22:37:33 +0100
committerEmilio Jesus Gallego Arias2019-02-23 16:53:53 +0100
commitd31056ec924ef6e09b28bc3822b427b67a8a300b (patch)
treed720333732d9be1a03f74cc079e0a1903d31e023 /dev/ci
parentc37e90b67c74b32837409a9a424757246067ef1b (diff)
[vernac] Unify declaration hooks.
Supersedes #8718.
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh12
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh
new file mode 100644
index 0000000000..27ce9aca16
--- /dev/null
+++ b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then
+
+ equations_CI_REF=hooks_unify
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ mtac2_CI_REF=hooks_unify
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+ paramcoq_CI_REF=hooks_unify
+ paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+fi