diff options
| -rw-r--r-- | .gitlab-ci.yml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c4aa195..4043ee5 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -10,13 +10,14 @@ before_script: build: stage: build script: - - opam pin add odoc --dev-repo + - echo "Build successful" only: - master pages: stage: deploy script: + - opam pin add odoc --dev-repo - dune build @doc - cp -r _build/default/_doc/_html/ public/ artifacts: |