diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-17 19:32:08 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-13 23:56:06 +0200 |
| commit | 4aaeb8abf89d504de44252ee9923bcba1e3eb007 (patch) | |
| tree | 648b261a2ec283c5765162cb25c2601fcba834d5 /.gitlab-ci.yml | |
| parent | e3eb17a728d7b6874e67462e8a83fac436441872 (diff) | |
[travis] Update testing to 4.05.0 + Camlp5 7.01
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e1feabd06..39189b483 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,8 +18,8 @@ variables: # some useful values COMPILER_32BIT: "4.02.3+32bit" - COMPILER_BLEEDING_EDGE: "4.04.1" - CAMLP5_VER_BLEEDING_EDGE: "6.17" + COMPILER_BLEEDING_EDGE: "4.05.0" + CAMLP5_VER_BLEEDING_EDGE: "7.01" COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" |