diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-28 23:47:34 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-28 23:47:34 +0200 |
commit | 9f05901696feba9c970c3385af08b4779aae9078 (patch) | |
tree | 55c0c3aec2459ef3f43321d791b2947f849bd243 /.gitlab-ci.yml | |
parent | a76730b8479b9036e814cc3ff5e7f32d46fc942c (diff) |
[doc] Remove unused dependencies.
AFAICS `imagemagick` `hacha` and `transfig` are not used anymore.
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d72a33e86..ad3d5e46d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -25,7 +25,7 @@ variables: #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" COQIDE_OPAM: "lablgtk-extras" 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 python3-pip" + COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript tipa python3-pip" COQDOC_OPAM: "hevea" SPHINX_PACKAGES: "bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex" ELPI_OPAM: "elpi" |