aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-11 20:14:45 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-12 16:24:04 +0200
commita069562bc0d4e82f6b1587864a8297b21a3250cc (patch)
treee53690330a5b3d417a40bc9f074c8fb5e64bb22e
parent77e3b3c43aebe9ad18ac99b34cf6dfac1ecc93fd (diff)
[warnings] Disable warning 58 "no cmx file was found in path"
-rw-r--r--configure.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 0b6b47e9a..3a98e8892 100644
--- a/configure.ml
+++ b/configure.ml
@@ -647,9 +647,10 @@ let camltag = match caml_version_list with
48: implicit elimination of optional arguments: too common
50: unexpected documentation comment: too common and annoying to avoid
56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3
+ 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
59: "potential assignment to a non-mutable value": See Coq's issue #8043
*)
-let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-59"
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59"
let coq_warn_error =
if !prefs.warn_error
then "-warn-error +a"