From ed0e9a0e16dc1f80ce8c45725aea9cead7bbc49c Mon Sep 17 00:00:00 2001 From: Thibault Martin <thi.martin.pro@pm.me> Date: Fri, 29 Mar 2024 11:48:17 +0100 Subject: [PATCH] Add an option in test script to launch Dune in watch mode --- bin/test.sh | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/bin/test.sh b/bin/test.sh index adfc3e9ea90..be51144b495 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 -- GitLab