diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 15:41:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 15:42:10 +0200 |
| commit | 65b1c7a4f516ff1f60b39dd36c8ba967df18f84c (patch) | |
| tree | 35c725be3ead44450fb58a228a3be17c96163d76 /Makefile.doc | |
| parent | 15378584beffa63d83b4f443b4ec60c306efaadc (diff) | |
Fix gitlab ubuntu version
Newer versions don't have the latex packages we want.
see eg https://gitlab.com/SkySkimmer/coq/-/jobs/65498131
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions