From 9e0b84ecfdd0e8f7e8eb15e66f48cbcc8ced55c1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 9 Jun 2023 23:13:18 -0400 Subject: [PATCH] makefile --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 2428bca..f01440d 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,7 @@ all: build test build: - @dune build @all + @dune build @install test: @dune runtest --no-buffer --force @@ -13,7 +13,7 @@ clean: doc: @dune build @doc -WATCH?=@all +WATCH?= @install @runtest watch: @dune build $(WATCH )-w