Merge branch 'fix/dune-typetree-git-repo' into 'master'

[installexternal.sh] Adapt path for dune-typetree installation

See merge request !415

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