chore: makefile

This commit is contained in:
Simon Cruanes 2023-09-13 14:18:57 -04:00
parent af71df8daf
commit a32e8638ee
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4

View file

@ -1,5 +1,6 @@
OPTS="--profile=release --ignore-promoted-rules" OPTS=--profile=release --ignore-promoted-rules
all: all:
@dune build @all $(OPTS) @dune build @all $(OPTS)