aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAdelyn Breedlove <[email protected]>2019-03-02 18:40:33 -0700
committerAdelyn Breedlove <[email protected]>2019-03-02 18:40:33 -0700
commit236f00b9bf43c607532077f430bf037304d5ff08 (patch)
treef85c20000ebb403bcb9fc96e77eaad238e8edad1
parentupdate opam file (diff)
parentAdd MRs to CI build (diff)
downloaddisml-236f00b9bf43c607532077f430bf037304d5ff08.tar.xz
disml-236f00b9bf43c607532077f430bf037304d5ff08.zip
Merge branch 'master' into lwt
-rw-r--r--.gitlab-ci.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 33c8611..6c1ec6a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -14,6 +14,7 @@ build:
- echo "Build successful"
only:
- master
+ - merge_requests
pages:
stage: deploy