diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh index e344e869d5..2b4c1489ad 100644 --- a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh +++ b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh @@ -7,6 +7,7 @@ if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; the mtac2_CI_REF="PR7819-overlay" mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 - Equations_CI_REF="PR7819-overlay" + equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + equations_CI_REF="PR7819-overlay" fi |