From 4138b1885a1cf581965248345d93f85091ab4844 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 20 Jun 2023 23:32:37 -0400 Subject: [PATCH] detail in makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 4da8a1e6..60530672 100644 --- a/Makefile +++ b/Makefile @@ -15,7 +15,7 @@ clean: doc: @dune build @doc -WATCH?= "@install @runtest" +WATCH?= @install @runtest watch: @dune build $(OPTS) $(WATCH) -w