diff options
Diffstat (limited to 'dev/ci/user-overlays')
9 files changed, 28 insertions, 15 deletions
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index af4a96f4ae..7716bcb59a 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,4 +1,4 @@ -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi diff --git a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh deleted file mode 100644 index 5c4dd1324f..0000000000 --- a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then - formal_topology_CI_BRANCH=ci - formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git - - HoTT_CI_BRANCH=coq-pr-1033 - HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git - - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh deleted file mode 100644 index c9f1272bed..0000000000 --- a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then - ltac2_CI_BRANCH=localityfixyou - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git -fi diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh new file mode 100644 index 0000000000..c2e3670380 --- /dev/null +++ b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then + Equations_CI_BRANCH=rm-local-polymorphic-flag + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations +fi diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh new file mode 100644 index 0000000000..78789a6fc5 --- /dev/null +++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then + HoTT_CI_BRANCH=check-poly-effects + HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git +fi diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh new file mode 100644 index 0000000000..9677b35253 --- /dev/null +++ b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then + Equations_CI_BRANCH=API-removal + Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git + coq_dpdgraph_CI_BRANCH=API-removal + coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git + ltac2_CI_BRANCH=API-removal + ltac2_CI_GITURL=https://github.com/gares/ltac2.git +fi diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh new file mode 100644 index 0000000000..8a50fb1111 --- /dev/null +++ b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then + Equations_CI_BRANCH=fix-6535 + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh new file mode 100644 index 0000000000..3a3ab44e03 --- /dev/null +++ b/dev/ci/user-overlays/06686-ccnv-no-proj.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then + Equations_CI_BRANCH=ccnv-fixes + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9146d3d521..9f0377ceea 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub Example: `00669-maximedenes-ssr-merge.sh` containing ``` -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi ``` + +(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh)) |