diff --git a/doc/scripts/filter-doc-log.sh b/doc/scripts/filter-doc-log.sh index 0fea74456..116ccf0d5 100755 --- a/doc/scripts/filter-doc-log.sh +++ b/doc/scripts/filter-doc-log.sh @@ -38,6 +38,7 @@ if [ -s "${LOG_FILE}" ]; then echo cat doc.warnings echo + exit 1 else echo -e "${green}No new errors/warnings." $TPUT sgr0