diff options
Diffstat (limited to 'dev/ci/user-overlays')
4 files changed, 19 insertions, 4 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/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh new file mode 100644 index 0000000000..575df07425 --- /dev/null +++ b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=pure-sharing-flag + +if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +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 ``` diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh new file mode 100644 index 0000000000..76aa37d380 --- /dev/null +++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then + HoTT_CI_REF=fix-for-numeral-notations + HoTT_CI_GITURL=https://github.com/JasonGross/HoTT + HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive +fi |