diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-16 10:27:49 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-16 10:27:49 +0100 |
| commit | 6bef869040014b4d589a8e49b42ac36a970d1bc6 (patch) | |
| tree | 1310b87acfeefa5b0d06d6c6b5e612ba9420befc /cparser | |
| parent | 15f354788a954635b44b3d2fae1057f67006509e (diff) | |
| download | compcert-kvx-6bef869040014b4d589a8e49b42ac36a970d1bc6.tar.gz compcert-kvx-6bef869040014b4d589a8e49b42ac36a970d1bc6.zip | |
Change warning for pragmas inside functions
Follow-up to 35e2b11db.
Put the warning "pragmas are ignored inside functions" inside the Unnamed
category, so that it is displayed by default and cannot be disabled.
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 2e02275c..25e4a980 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2872,7 +2872,7 @@ let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool) (* pragma *) | PRAGMA(s, loc) -> if local then - warning loc Unknown_pragmas "pragmas are ignored inside functions" + warning loc Unnamed "pragmas are ignored inside functions" else emit_elab env loc (Gpragma s); ([], env) |