From 65e876bebc6ed47eec002fd383e0515a614ae8f3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 30 Jul 2022 23:58:18 -0400 Subject: [PATCH] chore: makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 78dbae1b..9840b1d9 100644 --- a/Makefile +++ b/Makefile @@ -77,7 +77,7 @@ reindent: @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: " @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i -WATCH=@all +WATCH?=@all watch: dune build $(WATCH) -w $(OPTS) #@dune build @all -w # TODO: once tests pass