aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-02-23 17:38:44 -0500
committerEmilio Jesus Gallego Arias2020-03-29 23:49:26 -0400
commit4fa753561b2815f0455c455ac970759c2ac8ef7a (patch)
treebc4b55d451718b24d702206da1d7cafa6ca52910
parent6760a066168a5be0d3b479741fe8ac6c39339610 (diff)
[configure] Disable warning 67 which seems 100% bogus
-rw-r--r--configure.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index ee2e50ef86..eaa0e321b0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -616,8 +616,9 @@ let camltag = match caml_version_list with
45: "open" shadowing a label or constructor: see 44
48: implicit elimination of optional arguments: too common
58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
+ 67: "unused functor parameter" seems totally bogus
*)
-let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-58"
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-58-67"
let coq_warn_error =
if !prefs.warn_error
then "-warn-error +a"