diff --git a/bin/test.sh b/bin/test.sh index adfc3e9ea909cdc6cb46908df7b87b85e0ec564c..be51144b495c37c213c58683b086590dea3b713a 100755 --- a/bin/test.sh +++ b/bin/test.sh @@ -81,6 +81,7 @@ function Usage 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 " --watch run dune in watch mode." echo " --coverage compute test coverage in html format" echo " --coverage-xml compute test coverage in Cobertura XML format" echo " --coverage-json compute test coverage in Coveralls JSON format" @@ -171,6 +172,9 @@ do DUNE_OPT+="--auto-promote " UPDATE=yes ;; + "--watch") + DUNE_OPT+="--watch " + ;; "-v"|"--verbose") DUNE_OPT+="--display=short " VERBOSE=yes