diff options
| author | Emilio Jesus Gallego Arias | 2019-03-29 16:16:52 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-29 16:16:52 +0100 |
| commit | 379781acc56c430485088e6d67785d420fa69691 (patch) | |
| tree | 25523bbb0beb6678a4ce5c90219a956ed69ea68d /dev | |
| parent | 4b9636ffd47ea5a0b99df442047ba03d18422738 (diff) | |
| parent | 705b593287c787d4c2e71b01b76e6a66d1bbb517 (diff) | |
Merge PR #9853: Use only lowercase for unimath in CI scripts
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-unimath.sh | 4 |
2 files changed, 5 insertions, 5 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 diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index a7644fee23..704e278a4b 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download UniMath +git_download unimath -( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no ) +( cd "${CI_BUILD_DIR}/unimath" && make BUILD_COQ=no ) |