diff options
| author | Emilio Jesus Gallego Arias | 2017-10-09 16:12:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-10-10 10:47:58 +0200 |
| commit | 1d8725b59309c2c9f870eb52a2daebe87ed9ad5b (patch) | |
| tree | 5f7beb8ea5b420cbbcbad414e6f216b34d08b464 /dev | |
| parent | 406717ce786a70e64b9043db45dd5a2add68f817 (diff) | |
[flambda] [native] Pass `-Oclassic` to the native compiler.
This seems a safe choice as of today, but more advanced users would
like to tweak it, or we could even refine it by a configure option if
desired.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions