diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-27 23:49:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-10 10:47:31 +0200 |
| commit | 406717ce786a70e64b9043db45dd5a2add68f817 (patch) | |
| tree | f37eeae1efcc765045ff1851cb79518cb23bf4e1 /dev/doc | |
| 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 'dev/doc')
| -rw-r--r-- | dev/doc/changes.md | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index b5e19f33c..8a2a2fffc 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -40,6 +40,9 @@ Coq is compiled with `-safe-string` enabled and requires plugins to do the same. This means that code using `String` in an imperative way will fail to compile now. They should switch to `Bytes.t` +Configure supports passing flambda options, use `-flambda-opts OPTS` +with a flambda-enabled Ocaml to tweak the compilation to your taste. + ### ML API - Added two functions for declaring hooks to be executed in reduction |