diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-26 23:31:05 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-26 23:31:05 +0200 |
| commit | c65a1637b5e6cb60222963f29fc7c01bd7d1ee0b (patch) | |
| tree | e3f07a36afdd9f41873d0312f16db8bd08af8236 /Makefile.ci | |
| parent | 81f809cec470e2d1cfcf179333db859d00b3a728 (diff) | |
| parent | c4bc671db43246a8bfbe18d20fc954e640e42ff5 (diff) | |
Merge PR #7321: configure: make -annotate fatal, and color error and warnings
Diffstat (limited to 'Makefile.ci')
0 files changed, 0 insertions, 0 deletions