From fdb0f5c4e9ac41d387bd35c5a5cc9181d2841e3c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 9 Jun 2023 16:08:21 -0400 Subject: [PATCH] makefile: change default watch target --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index de0d203..30bbc57 100644 --- a/Makefile +++ b/Makefile @@ -12,7 +12,7 @@ test: doc: @dune build $(DUNE_OPTS) @doc -WATCH?=@all +WATCH?="@install @runtest" watch: dune build $(DUNE_OPTS) -w $(WATCH)