aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-10 15:54:38 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-10 15:54:38 +0200
commitf790c6ac8b16f71aae4868cbcad87a39f50727e3 (patch)
tree026665b355bf3c2712c3148b8e459e85ee10199a /dev
parent16f169b3c756aa3c5cbc38eb13412ba23ae2937d (diff)
parent1d8725b59309c2c9f870eb52a2daebe87ed9ad5b (diff)
Merge PR #540: [configure] Support for flambda flags.
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.md3
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