aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorGravatar Leonidas Lampropoulos <lemonidas_13@hotmail.com>2018-06-02 22:43:17 -0400
committerGravatar Leonidas Lampropoulos <lemonidas_13@hotmail.com>2018-06-02 22:43:17 -0400
commit3334a54c1e6e75a7d1080498e1ce58bd0ecb73bd (patch)
tree78624fb8e0adc92f130d51938bba4bec0c066b79 /.gitlab-ci.yml
parent5610d73c418de33b2248eb08074fd2de0383f596 (diff)
Update .gitlab to use newer ocaml
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b2d0d894f..a6eed661e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -343,7 +343,7 @@ ci-pidetop:
<<: *ci-template
ci-quickchick:
- <<: *ci-template
+ <<: *ci-template-flambda
ci-sf:
<<: *ci-template