diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7ae759756b765bdbc89c05b073930515816bc885..1f9985049d5f76999ad967dc5c3cefd201c228fb 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -142,7 +142,7 @@ build: # with the variable CLEAN_DUNE_CACHE set to "true". script: - - echo "Acquire::http::Proxy \"http://proxy.isae.fr:3128\"" | sudo tee /etc/apt/apt.conf > /dev/null + - echo "Acquire::http::Proxy \"http://proxy.isae.fr:3128\";" | sudo tee /etc/apt/apt.conf > /dev/null - if [ "$CLEAN_OPAM_CACHE" == "true" ]; then echo "we clean the _opam cache as explicitly requested"; rm -fR _opam; fi - if [ "$CLEAN_DUNE_CACHE" == "true" ]; then echo "we clean the dune _build cache as explicitly requested"; rm -fR _build; fi # Note: Gitlab supports multi-line scripts with "- |" or "- >", but the