update Armadillo repo URL

djm2131 · Jun 6, 2018 · 3421881 · 3421881
1 parent 14d4773
commit 3421881
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/configure b/configure
@@ -76,7 +76,7 @@ if [ -z ${ARMA_INCLUDE_PATH+x} ]; then
         echo ""
 
         mkdir ${WDIR}/arma_tmp
-        git clone -b unstable --single-branch https://github.com/conradsnicta/armadillo-code ${WDIR}/arma_tmp > /dev/null 2>&1
+        git clone -b unstable --single-branch https://gitlab.com/conradsnicta/armadillo-code.git ${WDIR}/arma_tmp > /dev/null 2>&1
         mv ${WDIR}/arma_tmp/include/* ${WDIR}/include
         rm -rf ${WDIR}/arma_tmp
         ARMA_INCLUDE_PATH="./include"