aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-29 16:16:52 +0100
committerEmilio Jesus Gallego Arias2019-03-29 16:16:52 +0100
commit379781acc56c430485088e6d67785d420fa69691 (patch)
tree25523bbb0beb6678a4ce5c90219a956ed69ea68d /dev/ci/ci-basic-overlay.sh
parent4b9636ffd47ea5a0b99df442047ba03d18422738 (diff)
parent705b593287c787d4c2e71b01b76e6a66d1bbb517 (diff)
Merge PR #9853: Use only lowercase for unimath in CI scripts
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index deeec3942d..62335ea5d0 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -24,9 +24,9 @@
########################################################################
# UniMath
########################################################################
-: "${UniMath_CI_REF:=master}"
-: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}"
-: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}"
+: "${unimath_CI_REF:=master}"
+: "${unimath_CI_GITURL:=https://github.com/UniMath/UniMath}"
+: "${unimath_CI_ARCHIVEURL:=${unimath_CI_GITURL}/archive}"
########################################################################
# Unicoq + Mtac2