From 3fad1bde82d573fdb0d82fa1158c4bcad7b30c4b Mon Sep 17 00:00:00 2001
From: Adelyn Breelove <tenseiken595@gmail.com>
Date: Mon, 4 Feb 2019 14:31:09 -0700
Subject: Oof, put CI script change in wrong job

---
 .gitlab-ci.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to '.gitlab-ci.yml')

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:
-- 
cgit v1.2.3