aboutsummaryrefslogtreecommitdiff
path: root/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-02-28 00:12:10 +0100
committerEmilio Jesus Gallego Arias2019-06-21 13:02:19 +0200
commit4a60c81e9fc67d98558b48d9f79e2d3610d60d77 (patch)
treebb3a21ec0911f87e8ffa9086a6482c67a65e41d0 /dune
parent623a431c293dcff42b4bc4dc3dc50c047a9ecbcc (diff)
[dune] Enable optimization options in the compilation of the VM.
So far we didn't setup optimization flags for the VM in the Dune build, but time has come to experiment with such flags, we try -O3. Enabling `-flto` in the final binary build would be great, however this seems to break windows.
Diffstat (limited to 'dune')
-rw-r--r--dune7
1 files changed, 7 insertions, 0 deletions
diff --git a/dune b/dune
index 4beba1c14f..6fb0612e4e 100644
--- a/dune
+++ b/dune
@@ -8,6 +8,13 @@
(ocaml409
(flags :standard -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60 -warn-error -5 -alert --deprecated)))
+; Information about flags for release mode:
+;
+; In #9665 we tried to add (c_flags -O3) to the release setup,
+; unfortunately the resulting VM seems to be slower [5% slower on
+; fourcolor, thus we keep the default C flags for now, which seem to
+; be -O2.
+
; The _ profile could help factoring the above, however it doesn't
; seem to work like we'd expect/like:
;