From fd760d44a3d172e8c20f26affb2373503ef0e760 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 9 Apr 2023 14:59:19 -0400 Subject: [PATCH] makefile --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index d874f3df..9120f4c0 100644 --- a/Makefile +++ b/Makefile @@ -30,9 +30,9 @@ update_next_tag: sed -i "s/NEXT_VERSION/$(VERSION)/g" $(wildcard src/**/*.ml) $(wildcard src/**/*.mli) sed -i "s/NEXT_RELEASE/$(VERSION)/g" $(wildcard src/**/*.ml) $(wildcard src/**/*.mli) -WATCH?="@src/all @tests/runtest" +WATCH?=@src/all @tests/runtest watch: - @dune build "$(WATCH)" -w + @dune build $(WATCH) -w reindent: @which ocp-indent || ( echo "require ocp-indent" ; exit 1 )