diff --git a/scripts/travis_script.sh b/scripts/travis_script.sh index c354bbb06..664582906 100755 --- a/scripts/travis_script.sh +++ b/scripts/travis_script.sh @@ -7,7 +7,7 @@ fi if [ ${TASK} == "doc" ]; then make doc 2>log.txt - (cat log.txt|grep warning) && exit -1 + (cat log.txt| grep -v ENABLE_PREPROCESSING |grep -v "unsupported tag" |grep warning) && exit -1 fi if [ ${TASK} == "build" ]; then