diff --git a/bin/test.sh b/bin/test.sh index 39cc55d2ff03d38a8d954f9c264bfcc1dacb353a..5b2da558ae516c3a0aa2f0b98fa967eb0dd75e9e 100755 --- a/bin/test.sh +++ b/bin/test.sh @@ -75,7 +75,8 @@ function Usage echo " -u|--update run tests and update oracles (and WP-cache)" echo " -s|--save save dune logs into $DUNE_LOG" echo " -v|--verbose print executed commands" - echo " -j|--jobs <jobs> Run no more than <jobs> commands simultaneously." + echo " -j|--jobs <jobs> run no more than <jobs> commands simultaneously." + echo " --coverage compute test coverage" echo " -h|--help print this help" echo "" echo "VARIABLES"