diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-16 16:10:42 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-16 16:10:42 +0100 |
| commit | edf1a8f36f75861b822081b3825357e122b6937d (patch) | |
| tree | 0a51bd6e5baeb0d48f7ab32402ace363875bb3da | |
| parent | 0786ae361cb5f134e91d790d6c096f84535b19ec (diff) | |
| parent | 09a269111a4b6736118aa82667bef3abc28bd281 (diff) | |
Merge PR #6160: Fix gitlab for 4.06
| -rw-r--r-- | .gitlab-ci.yml | 3 |
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 |