diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-15 13:52:40 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:56:35 +0200 |
| commit | 2d6ebc9d8bffd5910f201af75a0b3e45dd9c8988 (patch) | |
| tree | 442b19abba3293750f34c352995f82843c11006e | |
| parent | 633e40b6f925556e94347c348a2804cdc1068d88 (diff) | |
[travis] Overlay for PR#461: Camlp4 removal.
| -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..bb193ebb5 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 == "461" ] || [ $TRAVIS_BRANCH == "stm+remove_compat_parsing" ]; then + mathcomp_CI_BRANCH=no_camlp4_compat + mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git +fi |