aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2020-03-12 13:33:12 +0100
committerThéo Zimmermann2020-03-12 13:33:12 +0100
commit1534ae991ad44db8da9394f1d1ae0f240da6b541 (patch)
tree7ea4c9fde9b20890d0eac6cdbe008fe741a5a55a
parentaf1b164b2a496d9c44b4b8648e37514b3def5b7a (diff)
parent12ae13cf2d90b2f8a3a26274235284aae60646c5 (diff)
Merge PR #11810: [dune] Fix ocamlopt_flags for release profile
Reviewed-by: Zimmi48
-rw-r--r--dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/dune b/dune
index a3d596af48..d59346ed68 100644
--- a/dune
+++ b/dune
@@ -2,7 +2,7 @@
(env
(dev (flags :standard -rectypes -w -9-27+40+60 \ -short-paths))
(release (flags :standard -rectypes)
- (ocamlopt_flags -O3 -unbox-closures))
+ (ocamlopt_flags :standard -O3 -unbox-closures))
(ireport (flags :standard -rectypes -w -9-27-40+60)
(ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)))