diff options
Diffstat (limited to 'bashrc')
| -rw-r--r-- | bashrc | 9 |
1 files changed, 7 insertions, 2 deletions
@@ -41,8 +41,13 @@ cov() { local key=$cov/key local html=$cov/html local htmlfin=bin/cov - local gcov=$(which $(build $@ -qand1 variant=coverage | grep -w compile | \ - sed -n "s/.*\/gcc-\([0-9]\+\.[0-9]\+\.[0-9]\+\)\/.*/gcov-\1/p" | head -n1)) + local gcov=$(build $@ -qand1 variant=coverage | grep -w compile | \ + sed -n "s/.*\/gcc-\([0-9.]\+\)\/.*/gcov-\1/p" | head -n1) + if [[ -z $gcov ]] ; then + echo "Couldn't figure a gcov version" + return 1 + fi + gcov=$(find ${PATH//:/ } -name "$gcov*" 2> /dev/null | sort -Vr | head -n1) if [[ ! -x $gcov ]] ; then echo "Couldn't find a suitable gcov" return 1 |