From 705b593287c787d4c2e71b01b76e6a66d1bbb517 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 28 Mar 2019 14:22:51 +0100
Subject: Use only lowercase for unimath in CI scripts

Fix #9845
---
 dev/ci/ci-unimath.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/ci/ci-unimath.sh')

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 )
-- 
cgit v1.2.3