diff options
| author | Emilio Jesus Gallego Arias | 2020-03-12 00:48:07 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-12 00:51:44 -0400 |
| commit | 12ae13cf2d90b2f8a3a26274235284aae60646c5 (patch) | |
| tree | fd1636dd30409c541bd001d0d5451db084049d23 /dune | |
| parent | affb2fd89073accaa79ff6c2e468eb1bb9bd96bb (diff) | |
[dune] Fix ocamlopt_flags for release profile
Closes #11758
It turns out that we were overwriting the default `ocamlopt_flags`,
thus creating a problem in the release build.
Diffstat (limited to 'dune')
| -rw-r--r-- | dune | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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))) |