diff options
| author | coqbot-app[bot] | 2020-12-14 15:18:11 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-14 15:18:11 +0000 |
| commit | d5ca91cc6989759f0a467644a47979413f2c1f47 (patch) | |
| tree | 570b3e020bbf1af647f99981ce24e92c233d6679 /dev | |
| parent | d0667eb4a165c065b0d64069641ca0cd39d62219 (diff) | |
| parent | 1c667f5c1caf828f7dbf3e9c7910b8a0b7b84d03 (diff) | |
Merge PR #13626: [ci] update doc for overlays
Reviewed-by: Zimmi48
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/README.md | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 14ee5e4199..cf1d71c1cd 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -5,27 +5,29 @@ 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. 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. - +version so that testing is possible. 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: `13128-SkySkimmer-noinstance.sh` containing +This file must contain one or more invocation of the `overlay` function: +``` +overlay <project> <giturl> <ref> <prnumber> [<prbranch>] +``` +Each call creates an overlay for `project` using a given `giturl` and +`ref` which is active for `prnumber` or `prbranch` (`prbranch` defaults +to `ref`). +Example of an overlay for the project `elpi` that uses the branch `noinstance` +from the fork of `SkySkimmer` and is active for pull request `13128` ``` overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128 ``` -See [`ci-common.sh`](../ci-common.sh) for the detailed documentation of -the `overlay` function. +Such a file can be created automatically using the scripts +[`create_overlays.sh`](../../dev/tools/create_overlays.sh). +See also the list of projects for which one can write an overlay in +the file [`ci-basic-overlay.sh`](../ci-basic-overlay.sh). ### Branching conventions |