diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 0285747432..ab2d2e382c 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -20,3 +20,12 @@ # the name of the branch from which the PR originated. "" if the # current job is a push build. +echo $TRAVIS_PULL_REQUEST_BRANCH +echo $TRAVIS_PULL_REQUEST +echo $TRAVIS_BRANCH +echo $TRAVIS_COMMIT + +if [ $TRAVIS_PULL_REQUEST == "379" ] || [ $TRAVIS_BRANCH == "pr379" ]; then + mathcomp_CI_BRANCH=econstr + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git +fi |