diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-common.sh | 13 | ||||
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 6 |
2 files changed, 14 insertions, 5 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2711b7ecaa..f1e1515d41 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -2,11 +2,18 @@ set -xe +if [ -n "${GITLAB_CI}" ]; +then + export COQBIN=`pwd`/install/bin +else + export COQBIN=`pwd`/bin +fi +export PATH="$COQBIN:$PATH" + # Coq's tools need an ending slash :S, we should fix them. -export COQBIN=`pwd`/bin/ -export PATH=`pwd`/bin:$PATH +export COQBIN="$COQBIN/" -ls `pwd`/bin +ls "$COQBIN" # Where we clone and build external developments CI_BUILD_DIR=`pwd`/_build_ci diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 1f7fbcbf68..bfa43cde1d 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,8 +25,10 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT -if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then - mathcomp_CI_BRANCH=options+remove_non_sync +if [ $TRAVIS_PULL_REQUEST == "678" ] || [ $TRAVIS_BRANCH == "coqlib-part-02" ]; then + + mathcomp_CI_BRANCH=coqlib-part-02 mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git + fi |