diff options
| -rwxr-xr-x | tools/proof | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/tools/proof b/tools/proof index aec67146..c0798575 100755 --- a/tools/proof +++ b/tools/proof @@ -36,10 +36,18 @@ function build_and_test() { exit 1 fi - echo %%% Testing $NAME %%% - if ! (cd $DIR && make fullcheck); then - echo %%% FAILED to test $NAME %%% - exit 1 + if [ "$NAME" = "gcov" ]; then + echo %%% Testing $NAME %%% + if ! (cd $DIR && make check); then + echo %%% FAILED to test $NAME %%% + exit 1 + fi + else + echo %%% Testing $NAME %%% + if ! (cd $DIR && make fullcheck); then + echo %%% FAILED to test $NAME %%% + exit 1 + fi fi } |