aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-05-05 14:11:12 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-05-17 09:12:40 +0200
commit8252ff7ef7159a2493dd5ac76a647a8b96a5a692 (patch)
tree7854aa6287420275c4db1bae468f09bf24f1cd22
parentf6b0d8b78ae25c8b1c6b901e57a5f4e38f20cdbd (diff)
Travis: deduplicate package list for coqide+documentation targets
-rw-r--r--.travis.yml18
1 files changed, 2 insertions, 16 deletions
diff --git a/.travis.yml b/.travis.yml
index 8dcc34a8d..158f61cfd 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -65,7 +65,7 @@ matrix:
apt:
sources:
- avsm
- packages:
+ packages: &extra-packages
- opam
- aspcud
- libgtk2.0-dev
@@ -90,21 +90,7 @@ matrix:
apt:
sources:
- avsm
- packages:
- - opam
- - aspcud
- - libgtk2.0-dev
- - libgtksourceview2.0-dev
- - texlive-latex-base
- - texlive-latex-recommended
- - texlive-latex-extra
- - texlive-math-extra
- - texlive-fonts-recommended
- - texlive-fonts-extra
- - latex-xcolor
- - ghostscript
- - transfig
- - imagemagick
+ packages: *extra-packages
install:
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y