aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-27 23:49:09 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-10 10:47:31 +0200
commit406717ce786a70e64b9043db45dd5a2add68f817 (patch)
treef37eeae1efcc765045ff1851cb79518cb23bf4e1 /config
parentf927df44202034fa8cf73f72af876ae1e4ca05ba (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 'config')
-rw-r--r--config/coq_config.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 429d8811b..885b3ef4c 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -72,6 +72,8 @@ val gtk_platform : [`QUARTZ | `WIN32 | `X11]
val has_natdynlink : bool
val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *)
+val flambda_flags : string list
+
val wwwcoq : string
val wwwrefman : string
val wwwbugtracker : string