diff options
Diffstat (limited to 'dev/ci/ci-geocoq.sh')
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 8c57318477..e4fc983e68 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -5,6 +5,6 @@ ci_dir="$(dirname "$0")" install_ssralg -git_download GeoCoq +git_download geocoq -( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make ) +( cd "${CI_BUILD_DIR}/geocoq" && ./configure.sh && make ) |