aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-14 11:28:16 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-14 15:07:00 +0100
commitb63abc6b93f458bc7a2a16b45b8941a34c25cb03 (patch)
tree17ca1c180d4ad594ea9803ff04bb681ad08fdf38 /configure.ml
parentf824657b2b0b42ff02d0c07337db1607e13f359f (diff)
[build] Build Coq and plugins with `-strict-sequence`
Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins.
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index c08e8dfcc..7fd900d99 100644
--- a/configure.ml
+++ b/configure.ml
@@ -475,6 +475,7 @@ let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else ""
(* This variable can be overriden only for debug purposes, use with
care. *)
let coq_safe_string = "-safe-string"
+let coq_strict_sequence = "-strict-sequence"
let cflags = "-Wall -Wno-unused -g -O2"
@@ -661,7 +662,7 @@ let coq_warn_error =
(* Flags used to compile Coq and plugins (via coq_makefile) *)
let caml_flags =
- Printf.sprintf "-thread -rectypes %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string
+ Printf.sprintf "-thread -rectypes %s %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string coq_strict_sequence
(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
let coq_caml_flags =