From 16b306c19a6b9eb55b4ec2ff4044b0f39f7c8999 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 29 Mar 2022 22:54:29 -0400 Subject: [PATCH] chore: in makefile, compile everything in release mode --- Makefile | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 85661a75..a9b267e0 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 @@ -14,8 +15,9 @@ clean: doc: @dune build @doc +WATCH?=@all watch: - @dune build @all -w + @dune build $(OPTS) $(WATCH) -w .PHONY: benchs tests build watch