diff options
| author | coqbot-app[bot] | 2020-10-23 08:35:52 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-23 08:35:52 +0000 |
| commit | 16180bf8a37f65acd7d15c5bac634984c813259e (patch) | |
| tree | 97697c2c9aff8ec31b642ae35ddba90428325f35 /dev/ci/user-overlays/README.md | |
| parent | 00b82b7399ce01730371b8e80315f65e9254da91 (diff) | |
| parent | c4f5d75bfef926c186272e2be5bdd1968db3fe88 (diff) | |
Merge PR #13177: Automatically merge overlays with most recent upstream version
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/ci/user-overlays/README.md')
| -rw-r--r-- | dev/ci/user-overlays/README.md | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 4c2f264a74..3f9ad5e878 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -4,15 +4,12 @@ When your pull request breaks an external project we test in our CI and you have prepared a branch with the fix, you can add an "overlay" to your pull 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 / 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. +An overlay is a file which defines where to look for the patched +version so that testing is possible. This is done by calling the +`overlay` command for each project with the project name (as used in +the variables in [`ci-basic-overlay.sh`](../ci-basic-overlay.sh)), the +location of your fork and the branch containing the patch on your +fork. Moreover, the file contains very simple logic to test the pull request number or branch name and apply it only in this case. @@ -21,13 +18,12 @@ The name of your overlay file should start with a five-digit pull request number, followed by a dash, anything (for instance your GitHub nickname and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). -Example: `10185-SkySkimmer-instance-no-bang.sh` containing +Example: `13128-SkySkimmer-noinstance.sh` containing ``` -if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then +if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then - quickchick_CI_REF=instance-no-bang - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance fi ``` |