diff options
Diffstat (limited to 'dev/ci/ci-user-overlay.sh')
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 2ecd40416..b242ce3bd 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -33,10 +33,6 @@ fi echo "DEBUG: ci-user-overlay.sh 0" if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then echo "DEBUG: ci-user-overlay.sh 1" - bedrock_src_CI_BRANCH=trunk__API - bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git - bedrock_facade_CI_BRANCH=trunk__API - bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git fiat_parsers_CI_BRANCH=trunk__API fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git fi |