diff options
Diffstat (limited to 'dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh')
| -rw-r--r-- | dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh deleted file mode 100644 index 12be1b676a..0000000000 --- a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh +++ /dev/null @@ -1,12 +0,0 @@ -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 |