summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrei Karas <akaras@inbox.ru>2017-05-19 02:42:39 +0300
committerAndrei Karas <akaras@inbox.ru>2017-05-19 02:42:39 +0300
commitd15cae786b30986685917b92b7764ee38c20d370 (patch)
tree5ff7f1e4013007846a9f28b67766ffce8de7b88e
parent2dd0a701b8cca42e8fae6a4c4c15c5b14c3d8582 (diff)
downloadplus-d15cae786b30986685917b92b7764ee38c20d370.tar.gz
plus-d15cae786b30986685917b92b7764ee38c20d370.tar.bz2
plus-d15cae786b30986685917b92b7764ee38c20d370.tar.xz
plus-d15cae786b30986685917b92b7764ee38c20d370.zip
Exclude doctest.h from mplint checks.
-rwxr-xr-xtools/ci/scripts/init.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh
index 99e6e2ac5..927ccebfd 100755
--- a/tools/ci/scripts/init.sh
+++ b/tools/ci/scripts/init.sh
@@ -276,7 +276,7 @@ function run_tarball {
function run_mplint {
rm $ERRFILE
echo "mplint/src/mplint $*"
- mplint/src/mplint $* >$ERRFILE
+ mplint/src/mplint $* | grep -v "src/test/doctest.h" >$ERRFILE
check_error $?
run_check_warnings
}