diff options
| author | Emilio Jesus Gallego Arias | 2018-09-01 01:56:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-01 01:56:30 +0200 |
| commit | 6f1c4ac389e595e09fdf4653847d8c3ccca0befb (patch) | |
| tree | 948a6a1ea0328b01925d7ee9120a82cc3d14317c /dev/ci/user-overlays | |
| parent | 166a3838a7f07df4181617e111ffeb67dd817929 (diff) | |
| parent | 04542c3288b838c57253f2c315f1dab028412a40 (diff) | |
Merge PR #8348: Download tarball instead of cloning external projects.
Diffstat (limited to 'dev/ci/user-overlays')
6 files changed, 6 insertions, 28 deletions
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index e6a2c4460b..d812df3ec0 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,6 +1,6 @@ #!/bin/sh if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh deleted file mode 100644 index 27f588e214..0000000000 --- a/dev/ci/user-overlays/07859-printers.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then - Equations_CI_BRANCH=fix-printers - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations -fi diff --git a/dev/ci/user-overlays/07908-proj-mind.sh b/dev/ci/user-overlays/07908-proj-mind.sh deleted file mode 100644 index 293eeb5a5a..0000000000 --- a/dev/ci/user-overlays/07908-proj-mind.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7908" ] || [ "$CI_BRANCH" = "proj-mind" ]; then - Equations_CI_BRANCH=fix-proj-mind - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations -fi diff --git a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh deleted file mode 100644 index 56c0dc3433..0000000000 --- a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7941" ] || [ "$CI_BRANCH" = "jun-27-missing-record-field-error-message-quickfix" ]; then - Equations_CI_BRANCH=overlay-question-mark-extended-for-missing-record-field - Equations_CI_GITURL=https://github.com/bollu/Coq-Equations -fi diff --git a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh deleted file mode 100644 index 99a11b9fbf..0000000000 --- a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8063" ] || [ "$CI_BRANCH" = "string-eqb" ]; then - quickchick_CI_BRANCH=fix-for-pr-8063 - quickchick_CI_GITURL=https://github.com/JasonGross/QuickChick -fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index d38d1b06d1..68afe7ee4a 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,10 +7,12 @@ request to test it with the adapted version of the external project. An overlay is a file which defines where to look for the patched version so that testing is possible. It redefines some variables from [`ci-basic-overlay.sh`](../ci-basic-overlay.sh): -give the name of your branch using a `_CI_BRANCH` variable and the location of -your fork using a `_CI_GITURL` variable. +give the name of your branch / commit using a `_CI_REF` variable and the +location of your fork using a `_CI_GITURL` variable. The `_CI_GITURL` variable should be the URL of the repository without a trailing `.git`. +If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is +necessary to redefine the `_CI_ARCHIVEURL` variable as well. Moreover, the file contains very simple logic to test the pull request number or branch name and apply it only in this case. @@ -25,7 +27,7 @@ Example: `00669-maximedenes-ssr-merge.sh` containing #!/bin/sh if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` |