diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 17:37:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-12 15:12:59 +0200 |
| commit | c05283cb80f81c521bb3a0d8e742d693b7db1a64 (patch) | |
| tree | fe263de62bcd6cafb85b9ae0151188d3e16a8e8b /configure.ml | |
| parent | 31fce698ec8c3186dc6af49961e8572e81cab50b (diff) | |
[ci] Remove warning jobs in favor of default `-warn-error yes`
As discussed in #6930, we remove the warnings jobs and instead do
require the developers to submit a clean build.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions