aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAdelyn Breelove <[email protected]>2019-02-04 14:31:09 -0700
committerAdelyn Breelove <[email protected]>2019-02-04 14:31:09 -0700
commit3fad1bde82d573fdb0d82fa1158c4bcad7b30c4b (patch)
treeeb66e7fba5bb66d01307c4f60a3769e37e3109a5
parentUpdate to latest master on ppx_deriving_yojson (diff)
downloaddisml-3fad1bde82d573fdb0d82fa1158c4bcad7b30c4b.tar.xz
disml-3fad1bde82d573fdb0d82fa1158c4bcad7b30c4b.zip
Oof, put CI script change in wrong job
-rw-r--r--.gitlab-ci.yml3
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: