diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 16:59:01 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 17:24:01 +0200 |
| commit | 133ac4fbb9a8b4213cb3f8ca2f7c2568931209ce (patch) | |
| tree | 9cd2726c9f2b73d424432b973fc4c8a5d3517fdb /dev/ci | |
| parent | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (diff) | |
Overlay for reference removal
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/07797-rm-reference.sh | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/07797-rm-reference.sh b/dev/ci/user-overlays/07797-rm-reference.sh new file mode 100644 index 000000000..f7811cd6f --- /dev/null +++ b/dev/ci/user-overlays/07797-rm-reference.sh @@ -0,0 +1,20 @@ +_OVERLAY_BRANCH=rm-reference + +if [ "$CI_PULL_REQUEST" = "7797" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations.git + + ltac2_CI_BRANCH="fix-7797" + ltac2_CI_GITURL=https://github.com/ppedrot/Ltac2.git + + quickchick_CI_BRANCH="$_OVERLAY_BRANCH" + quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick.git + + coq_dpdgraph_CI_BRANCH="$_OVERLAY_BRANCH" + coq_dpdgraph_CI_GITURL=https://github.com/maximedenes/coq-dpdgraph.git + + Elpi_CI_BRANCH="$_OVERLAY_BRANCH" + Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi.git + +fi |