diff options
| author | mdenes | 2013-01-24 08:06:42 +0000 |
|---|---|---|
| committer | mdenes | 2013-01-24 08:06:42 +0000 |
| commit | 9d1753b54f205f5c4b9489d8865aff877a4db6fa (patch) | |
| tree | 2021b065405f9482f2317c9f7db9fa5bca384901 /kernel/nativelib.ml | |
| parent | cff6778a03af680681e08726e352b735e0202066 (diff) | |
Native compiler: warnings were not turned off for OCaml 3.11
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16140 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index f8474bf199..86fe45bdc4 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -65,7 +65,7 @@ let call_compiler ml_filename load_path = let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in let comp_cmd = - Format.sprintf "%s -%s -o %s -rectypes -w -A -I %s %s" + Format.sprintf "%s -%s -o %s -rectypes -w a -I %s %s" compiler_name (if Dynlink.is_native then "shared" else "c") (Filename.quote link_filename) include_dirs (Filename.quote ml_filename) in |