diff --git a/Makefile b/Makefile index 85661a75..de348c88 100644 --- a/Makefile +++ b/Makefile @@ -14,8 +14,9 @@ clean: doc: @dune build @doc +WATCH?= "@install @runtest" watch: - @dune build @all -w + @dune build $(WATCH) -w .PHONY: benchs tests build watch