From 70cf95d90656e94b6121ad1ef9e0823e5042c11e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 8 Mar 2022 11:16:16 -0500 Subject: [PATCH] tweak script --- echo.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/echo.sh b/echo.sh index c97ce729..0f6cf2d7 100755 --- a/echo.sh +++ b/echo.sh @@ -1,2 +1,2 @@ #!/bin/sh -exec dune exec "examples/echo.exe" -- $@ +exec dune exec --profile=release "examples/echo.exe" -- $@