diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-25 00:00:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-25 00:00:18 +0100 |
| commit | 98e51078fa624ce780b16d8e372ef33ac97ffaee (patch) | |
| tree | 958e1b5d9e03143a8d03b25bda671a5f7a650d4c /dev | |
| parent | 486acdd7b50d4fdc0956011b7b48dc6ba96dd4a8 (diff) | |
Mathcomp overlay.
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 028574743..ab2d2e382 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 |