From a32e8638ee74b7852159ae163dc5ff2059ec1210 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 13 Sep 2023 14:18:57 -0400 Subject: [PATCH] chore: makefile --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index fdb7b173..d20dde92 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,6 @@ -OPTS="--profile=release --ignore-promoted-rules" +OPTS=--profile=release --ignore-promoted-rules + all: @dune build @all $(OPTS)