diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 594e3c3744..200d431bcb 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -44,4 +44,6 @@ fi if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then math_classes_CI_BRANCH=external-bignums math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git + Corn_CI_BRANCH=external-bignums + Corn_CI_GITURL=https://github.com/letouzey/corn.git fi |