diff options
| author | Emilio Jesus Gallego Arias | 2016-06-27 23:49:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-10-10 10:47:31 +0200 |
| commit | 406717ce786a70e64b9043db45dd5a2add68f817 (patch) | |
| tree | f37eeae1efcc765045ff1851cb79518cb23bf4e1 /kernel | |
| parent | f927df44202034fa8cf73f72af876ae1e4ca05ba (diff) | |
[configure] Support for flambda flags.
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions