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