aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2018-06-03 17:29:15 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-06-04 16:30:23 +0200
commit545df304d7c17acc475fb1b37f16959fcc430f6a (patch)
treede41fca799921eee32d345a6f9c5944667d1869a
parent4a11a47faff0bad5f7f3d65b3c00569ba983414d (diff)
downloadcompcert-kvx-545df304d7c17acc475fb1b37f16959fcc430f6a.tar.gz
compcert-kvx-545df304d7c17acc475fb1b37f16959fcc430f6a.zip
Turn off the warning "C11 extension" by default
These are extensions w.r.t. C99, not incompatible changes. Nothing bad can happen if those C11 features are used, except making the code incompatible with C99.
-rw-r--r--cparser/Diagnostics.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index 91acd161..0ab2c1e4 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -99,7 +99,6 @@ type warning_type =
let active_warnings: warning_type list ref = ref [
Unnamed;
Unknown_attribute;
- Celeven_extension;
Gnu_empty_struct;
Missing_declarations;
Constant_conversion;