diff options
| author | Maxime Dénès | 2018-03-08 21:25:38 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-08 21:25:38 +0100 |
| commit | 2f9a5ba5b952ab2c660bf465aae71f383198804c (patch) | |
| tree | 93b25a6bf173590fc8d1b12b04a5ed0e707dc0ce | |
| parent | 374d1efc5de20f8c99c13a7216357a7228c353e8 (diff) | |
| parent | 90df0b3b217d4c588c236d1e56639320401f7aff (diff) | |
Merge PR #6928: gitlab: install num for all 4.06 jobs
| -rw-r--r-- | .gitlab-ci.yml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5dd3760793..04b75bfdf6 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 |