diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-21 00:35:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-11 22:26:11 +0100 |
| commit | 4a72f3bfe23edaa87307449b6033e7a296a93b04 (patch) | |
| tree | ea6d8744f99fcc989c8bc744cea65a9b45e6eb05 /dev/ci | |
| parent | 213b32325eb8d98133dc7a7f47f14d2d7af79a53 (diff) | |
Adding a custom Travis overlay for HoTT.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh new file mode 100644 index 000000000..78789a6fc --- /dev/null +++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then + HoTT_CI_BRANCH=check-poly-effects + HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git +fi |