From 2d081c554bda09ac11c6675ce39f3fd6e70f6e8a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 2 Aug 2021 21:34:37 -0400 Subject: [PATCH] chore: fix makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b784d448..5b073ab0 100644 --- a/Makefile +++ b/Makefile @@ -70,7 +70,7 @@ reindent: WATCH=@all watch: - @dune build $(WATCH) -w $(OPTS) --profile=release + @dune build $(WATCH) -w $(OPTS) #@dune build @all -w # TODO: once tests pass .PHONY: clean doc all bench install uninstall remove reinstall bin test