diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:49:12 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:49:12 +0200 |
| commit | 2f75922ad52e334b7bcc3a26c2ecb1602c85fc2f (patch) | |
| tree | 3ba950c021df581a004a4af158880558eb2dbe14 /dev/ci | |
| parent | 03e4f9c3da333d13553b4ea3247b0c36c124995e (diff) | |
| parent | cb316573aa1d09433531e7c67e320c14ef05c3e2 (diff) | |
Merge PR#481: [option] Remove support for non-synchronous options.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 20 |
1 files changed, 2 insertions, 18 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 71d098e37..1f7fbcbf6 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,24 +25,8 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT -if [ $TRAVIS_PULL_REQUEST == "402" ] || [ $TRAVIS_BRANCH == "located_switch" ]; then - - mathcomp_CI_BRANCH=located_switch +if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then + mathcomp_CI_BRANCH=options+remove_non_sync mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git - - fiat_parsers_CI_BRANCH=located_switch - fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat.git - - bedrock_src_CI_BRANCH=located_switch - bedrock_src_CI_GITURL=https://github.com/ejgallego/bedrock.git - - bedrock_facade_CI_BRANCH=located_switch - bedrock_facade_CI_GITURL=https://github.com/ejgallego/bedrock.git - -fi - -if [ $TRAVIS_PULL_REQUEST == "406" ] || [ $TRAVIS_BRANCH == "feature/coq_makefile2" ]; then - UniMath_CI_BRANCH=master - UniMath_CI_GITURL=https://github.com/gares/UniMath.git fi |