Merge PR#730: Protecting from warnings while compiling 8.6

2 files changed, 4 insertions, 2 deletions

diff --git a/configure b/configure
index 09585e59ee..79c512f8a0 100755
--- a/configure
+++ b/configure
@@ -26,7 +26,7 @@ done
 
 ## We check that $cmd is ok before the real exec $cmd
 
-`$cmd -version > /dev/null 2>&1` && exec $cmd $script "$@"
+`$cmd -version > /dev/null 2>&1` && exec $cmd -w "-3" $script "$@"
 
 ## If we're still here, something is wrong with $cmd
 
diff --git a/configure.ml b/configure.ml
index 04b04979d9..caef75271c 100644
--- a/configure.ml
+++ b/configure.ml
@@ -510,6 +510,8 @@ let camltag = match caml_version_list with
   | x::y::_ -> "OCAML"^x^y
   | _ -> assert false
 
+let coq_warn_flag =
+  if caml_version_nums > [4;2;3] then "-w -3-52-56" else ""
 
 (** * CamlpX configuration *)
 
@@ -1128,7 +1130,7 @@ let write_makefile f =
   pr "CAMLHLIB=%S\n\n" camllib;
   pr "# Caml link command and Caml make top command\n";
   pr "# Caml flags\n";
-  pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
+  pr "CAMLFLAGS=-rectypes %s %s\n" coq_annotate_flag coq_warn_flag;
   pr "# User compilation flag\n";
   pr "USERFLAGS=\n\n";
   pr "# Flags for GCC\n";