diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9dd36cd..c4aa195 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -5,13 +5,12 @@ before_script: - opam init - eval `opam config env` - opam update - - opam pin add ppx_deriving_yojson https://github.com/ocaml-ppx/ppx_deriving_yojson.git#82bc0b8 - - opam pin add -d disml . + - opam pin add disml . build: stage: build script: - - echo "Build successful" + - opam pin add odoc --dev-repo only: - master |