From b8beba2201b81ebc6148bb96f3fcdd12cc425996 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gr=C3=A9goire=20Henry?= Date: Mon, 29 Jan 2018 22:54:20 +0100 Subject: [PATCH] CI: fix rule `publish:pages:` --- .gitlab-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 241c8bdb8..d7c8dcdee 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -410,7 +410,7 @@ publish:pages: - sudo apk update && sudo apk upgrade - sudo apk add py3-sphinx py3-sphinx_rtd_theme - sudo ln -s /usr/bin/sphinx-build-3 /usr/bin/sphinx-build - - opam install odoc + - opam install --yes odoc - make doc-html && sudo mv docs/_build "${CI_PROJECT_DIR}"/public tags: - gitlab-org