diff options
| author | Gaëtan Gilbert | 2019-03-28 14:22:51 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-28 14:44:34 +0100 |
| commit | 705b593287c787d4c2e71b01b76e6a66d1bbb517 (patch) | |
| tree | a66616ed6aae0b8b7316cdea220537541ba32b9f /dev/ci/ci-unimath.sh | |
| parent | 688e20c432d2639050a62703e1c566ddfbe42b2a (diff) | |
Use only lowercase for unimath in CI scripts
Fix #9845
Diffstat (limited to 'dev/ci/ci-unimath.sh')
| -rwxr-xr-x | dev/ci/ci-unimath.sh | 4 |
1 files changed, 2 insertions, 2 deletions
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 ) |