From ed0f016f274baf876d403037598431d92ec8944e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 5 Jun 2023 21:58:48 -0400 Subject: [PATCH] chore: makefile runs everything in release mode --- Makefile | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index de348c88..4da8a1e6 100644 --- a/Makefile +++ b/Makefile @@ -2,11 +2,12 @@ all: build test +OPTS?=--profile=release build: - @dune build @install + @dune build @install $(OPTS) test: - @dune runtest --no-buffer --force + @dune runtest --no-buffer --force $(OPTS) clean: @dune clean @@ -16,7 +17,7 @@ doc: WATCH?= "@install @runtest" watch: - @dune build $(WATCH) -w + @dune build $(OPTS) $(WATCH) -w .PHONY: benchs tests build watch