aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-05 12:11:22 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-05 12:11:22 +0200
commitf5a86aa6d18f569ac305559efd559ecad8f0b470 (patch)
treecc6e4c5d852ee84dc99cf9f9024c76b2fda1acd9 /dev/ci
parentaf65c79cc976f3f96a768f3d0897febb24e1485a (diff)
parentd4dac391db9e3be7a45d26e2da9007997b79587d (diff)
Merge PR #7099: Stronger invariants in unification signature.
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh4
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh
new file mode 100644
index 000000000..e6c48d10a
--- /dev/null
+++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then
+ Equations_CI_BRANCH=unification-returns-option
+ Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+fi