aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-06 15:59:28 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-07 19:51:43 +0100
commit90df0b3b217d4c588c236d1e56639320401f7aff (patch)
treed7a9eeecebbb27cf71949568d872f483417e3eba /.gitlab-ci.yml
parent67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff)
gitlab: install num for all jobs
Previously it was installed for the compilation jobs causing random failures when the other jobs got a cache without it.
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml4
1 files changed, 2 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5dd376079..04b75bfdf 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -26,7 +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"
+ COQIDE_OPAM_BE: "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"
@@ -49,7 +49,7 @@ before_script:
- opam switch ${COMPILER}
- eval $(opam config env)
- opam config list
- - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM}
+ - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM}
- rm -rf ~/.opam/log/
- opam list