blob: 76aa37d3806d35667611321c3eb0883092f863bb (
plain)
1
2
3
4
5
|
if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then
HoTT_CI_REF=fix-for-numeral-notations
HoTT_CI_GITURL=https://github.com/JasonGross/HoTT
HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive
fi
|
