From 1f61af068bdb69ae2063ff0847d2b1658718587e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 20 Jun 2023 22:45:43 -0400 Subject: [PATCH] chore: makefile --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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