diff options
| author | Emilio Jesus Gallego Arias | 2019-02-19 18:23:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-24 15:32:25 +0200 |
| commit | 728216337e2541b37135d86c1b0206706cf4ed1a (patch) | |
| tree | 8382ec1fa8615844792f2784a805d6bef2126f03 /lib/envars.ml | |
| parent | 75c5264aa687480c66a6765d64246b5ebd2c0d54 (diff) | |
[coq_makefile] Enforce warn_error for plugins.
The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.
As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.
We don't mark deprecation as fatal as to allow time for migration.
Fixes #6974
Diffstat (limited to 'lib/envars.ml')
| -rw-r--r-- | lib/envars.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index 0f4670688b..af8e45b137 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -178,6 +178,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; + fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3"; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) |