diff options
author | Leonidas Lampropoulos <lemonidas_13@hotmail.com> | 2018-06-02 22:43:17 -0400 |
---|---|---|
committer | Leonidas Lampropoulos <lemonidas_13@hotmail.com> | 2018-06-02 22:43:17 -0400 |
commit | 3334a54c1e6e75a7d1080498e1ce58bd0ecb73bd (patch) | |
tree | 78624fb8e0adc92f130d51938bba4bec0c066b79 /.gitlab-ci.yml | |
parent | 5610d73c418de33b2248eb08074fd2de0383f596 (diff) |
Update .gitlab to use newer ocaml
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r-- | .gitlab-ci.yml | 2 |
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 |