aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml3
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3117b2b9a..fcf6413be 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -26,6 +26,7 @@ variables:
COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev"
#COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386"
COQIDE_OPAM: "lablgtk-extras"
+ COQIDE_OPAM_BE: "num lablgtk.2.18.6 lablgtk-extras.1.6"
COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa"
COQDOC_OPAM: "hevea"
@@ -183,6 +184,7 @@ build:bleeding-edge:
<<: *build-variables
COMPILER: "$COMPILER_BLEEDING_EDGE"
CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
+ EXTRA_OPAM: "$COQIDE_OPAM_BE"
warnings:
<<: *warnings-template
@@ -200,6 +202,7 @@ warnings:bleeding-edge:
<<: *warnings-variables
COMPILER: "$COMPILER_BLEEDING_EDGE"
CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
+ EXTRA_OPAM: "$COQIDE_OPAM_BE"
test-suite:
<<: *test-suite-template