diff --git a/bin/installexternal.sh b/bin/installexternal.sh index 1cee08f5ac7647cb97cc10365be81e98d59838cf..fce3c517564ec156f87b49329a81b11edf688c82 100755 --- a/bin/installexternal.sh +++ b/bin/installexternal.sh @@ -391,7 +391,7 @@ installTypeTree() fi if [ ! -e dune-typetree ]; then - git clone -b releases/2.3 https://gitlab.dune-project.org/pdelab/dune-typetree.git + git clone -b releases/2.3 https://gitlab.dune-project.org/staging/dune-typetree.git fi if test "$DOWNLOAD_ONLY" == "y"; then