diff options
Diffstat (limited to 'tools/ci/scripts/init.sh')
| -rwxr-xr-x | tools/ci/scripts/init.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh index 8e84054ff..cd716cf94 100755 --- a/tools/ci/scripts/init.sh +++ b/tools/ci/scripts/init.sh @@ -217,9 +217,15 @@ function run_gcov { function run_check_warnings { if [[ -s "$ERRFILE" ]]; then + printf "Warnings detected in %s:\n" "$ERRFILE" cat $ERRFILE exit 1 fi + + if [[ -s "$ERRFILE_UNFILTERED" ]]; then + printf "Warnings detected in %s. The maintainer might want take a peek, sometimes.\n" \ + "$ERRFILE_UNFILTERED" + fi } function run_h { |