aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-14 17:09:45 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-19 17:46:51 +0100
commit1dcf5516ab772a6d5325d42c2ceaf727fe88bb86 (patch)
treea24c4ec3e89b2d7dc7805cbdf8e9d6c14d97bdc9 /.gitlab-ci.yml
parent06931bf4b193f978d43f30e22732b0122602ed53 (diff)
ci: add elpi
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml6
1 files changed, 6 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6b52870ce..5dd376079 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -285,6 +285,12 @@ ci-coquelicot:
<<: *ci-template-vars
EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"
+ci-elpi:
+ <<: *ci-template
+ variables:
+ <<: *ci-template-vars
+ EXTRA_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"
+
ci-equations:
<<: *ci-template