diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 2 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06686-ccnv-no-proj.sh | 4 |
3 files changed, 7 insertions, 1 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 628e892910..784da6f971 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -70,7 +70,7 @@ # Flocq ######################################################################## : "${Flocq_CI_BRANCH:=master}" -: "${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}" +: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq.git}" ######################################################################## # Coquelicot diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 05fa33e972..d7a356930e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -19,6 +19,8 @@ else then export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" + else # assume local + export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" fi export COQBIN="$PWD/bin" 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 |