diff options
| author | Emilio Jesus Gallego Arias | 2019-02-28 00:12:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-21 13:02:19 +0200 |
| commit | 4a60c81e9fc67d98558b48d9f79e2d3610d60d77 (patch) | |
| tree | bb3a21ec0911f87e8ffa9086a6482c67a65e41d0 /dev | |
| parent | 623a431c293dcff42b4bc4dc3dc50c047a9ecbcc (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 'dev')
0 files changed, 0 insertions, 0 deletions