aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Diagnostics.ml
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 /cparser/Diagnostics.ml
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.
Diffstat (limited to 'cparser/Diagnostics.ml')
-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;