chore: makefile

This commit is contained in:
Simon Cruanes 2023-06-20 22:45:43 -04:00
parent ac17e61a81
commit 1f61af068b
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4

View file

@ -14,8 +14,9 @@ clean:
doc:
@dune build @doc
WATCH?= "@install @runtest"
watch:
@dune build @all -w
@dune build $(WATCH) -w
.PHONY: benchs tests build watch