diff options
| author | Emilio Jesus Gallego Arias | 2018-10-09 14:28:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-11 15:23:00 +0200 |
| commit | 823f41dc9fa54efc7c55d3e1df8df7e5797837fb (patch) | |
| tree | 79e44f4f78923ec48206f09617c6a60cbdd50362 /kernel | |
| parent | 4a6ddf4fdc4790fc407dc98bcfb80fd816cab304 (diff) | |
[dune] Add optimizing flags to release profile.
- In `release` profile, we use an optimizing set of flags. This will
only affect to people using a Flambda-enabled OCaml.
- We use the `_` pattern for flags that are common to all profiles.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions