diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-28 16:33:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-28 16:33:41 +0200 |
| commit | a76730b8479b9036e814cc3ff5e7f32d46fc942c (patch) | |
| tree | 83f23277072f8cebe66fe7606f87eea85e5d3a1b | |
| parent | 75c144b25de008c85ff085761f80035a5a6278dd (diff) | |
| parent | 65b1c7a4f516ff1f60b39dd36c8ba967df18f84c (diff) | |
Merge PR #7376: Fix gitlab ubuntu version
| -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 7c5dea885..d72a33e86 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,4 +1,4 @@ -image: ubuntu:latest +image: ubuntu:xenial stages: - opam-boot |