From 58596a9bd51a997aaa0a72d8284698d028d54302 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 1 Apr 2023 20:07:51 -0400 Subject: [PATCH] chore: makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 9120f4c0..f77578bd 100644 --- a/Makefile +++ b/Makefile @@ -30,7 +30,7 @@ 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/check @tests/runtest watch: @dune build $(WATCH) -w