Merge branch 'ubuntu-eoan' into 'dev'

Build Ubuntu 19.10 instead of 19.04

See merge request ligolang/ligo!578
This commit is contained in:
Gabriel Alfour 2020-04-19 13:46:07 +00:00
commit c892c469f4
2 changed files with 4 additions and 4 deletions

View File

@ -40,7 +40,7 @@ dont-merge-to-master:
- build-and-package-debian-9
- build-and-package-debian-10
- build-and-package-ubuntu-18-04
- build-and-package-ubuntu-19-04
- build-and-package-ubuntu-19-10
before_script:
- export TERM=dumb
- scripts/install_native_dependencies.sh
@ -184,14 +184,14 @@ build-and-package-ubuntu-18-04:
- dev
- /^.*-run-dev$/
build-and-package-ubuntu-19-04:
build-and-package-ubuntu-19-10:
<<: *docker
# To run in sequence and save CPU usage, use stage: build_and_package_binaries
stage: test
variables:
target_os_family: "debian"
target_os: "ubuntu"
target_os_version: "19.04"
target_os_version: "19.10"
<<: *build_binary
only:
- dev

View File

@ -51,7 +51,7 @@ sudo apt install ./<package_name_here>.deb
```
- [Ubuntu 18.04](/deb/ligo_ubuntu-18.04.deb)
- [Ubuntu 19.04](/deb/ligo_ubuntu-19.04.deb)
- [Ubuntu 19.10](/deb/ligo_ubuntu-19.10.deb)
- [Debian 9](/deb/ligo_debian-9.deb)
- [Debian 10](/deb/ligo_debian-10.deb)