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 /.gitlab-ci.yml | |
| 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 '.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 e1c5b5255..f5b17f06f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,4 +1,4 @@ -image: ubuntu:latest +image: ubuntu:xenial stages: - opam-boot |