diff options
| author | Gaëtan Gilbert | 2018-04-28 15:41:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-04-28 15:42:10 +0200 |
| commit | 65b1c7a4f516ff1f60b39dd36c8ba967df18f84c (patch) | |
| tree | 35c725be3ead44450fb58a228a3be17c96163d76 /plugins/syntax | |
| 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 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions