blob: 12be1b676a9833e135009cf6476b564a47de7d46 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then
HoTT_CI_REF=rm-hardwired-hint-db
HoTT_CI_GITURL=https://github.com/vbgl/HoTT
ltac2_CI_REF=rm-hardwired-hint-db
ltac2_CI_GITURL=https://github.com/vbgl/ltac2
UniMath_CI_REF=rm-hardwired-hint-db
UniMath_CI_GITURL=https://github.com/vbgl/UniMath
fi
|
