diff options
Diffstat (limited to 'tools/ci/scripts')
| -rwxr-xr-x | tools/ci/scripts/init.sh | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tools/ci/scripts/init.sh b/tools/ci/scripts/init.sh index 944d4d338..c89717306 100755 --- a/tools/ci/scripts/init.sh +++ b/tools/ci/scripts/init.sh @@ -217,6 +217,13 @@ function run_make_check { echo "valgrind check" } +function run_gcov { + gcovr -r . --gcov-executable=$1 --html -o logs/$2.html + check_error $? + gcovr -r . --gcov-executable=$1 -o logs/$2.txt + check_error $? +} + function run_check_warnings { DATA=$(cat $ERRFILE) if [ "$DATA" != "" ]; |