diff options
| author | Théo Zimmermann | 2018-09-20 15:58:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 16:02:43 +0200 |
| commit | 968a72b6bc481916a67a2825d1fc245a2bb0071e (patch) | |
| tree | d1998c5649a3eb9e1a5ddc7d124790201d1946f2 /Makefile.dune | |
| parent | 5b01a356f1905af64353a5b60ec377df316d183a (diff) | |
Stop building LaTeX doc in Travis (keep HTML).
The LaTeX doc is already tested in GitLab CI and finding the right dependencies
in this older version of Ubuntu is a hurdle.
Diffstat (limited to 'Makefile.dune')
0 files changed, 0 insertions, 0 deletions