diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-03-07 09:56:58 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-03-10 18:54:45 +0100 |
| commit | c0df11e0c7495aa2e48bc4440eb1c4e844f4857d (patch) | |
| tree | c829c36a7676abd5f74bfabcb191b27aea0eb64a | |
| parent | 3ba79a0e18341806007ec091940eb1b8378ab739 (diff) | |
| download | compcert-c0df11e0c7495aa2e48bc4440eb1c4e844f4857d.tar.gz compcert-c0df11e0c7495aa2e48bc4440eb1c4e844f4857d.zip | |
Update warning flags used to compile Flocq and Menhirlib
We prefer not to change these two "vendored" libraries. Deprecation
warnings can only be addressed upstream. So let's silence them.
Flocq no longer triggers the `compatibility-notation` warning, so
let's not silence it.
| -rw-r--r-- | Makefile | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -193,8 +193,11 @@ endif proof: $(FILES:.v=.vo) -# Turn off some warnings for compiling Flocq -flocq/%.vo: COQCOPTS+=-w -compatibility-notation +# Turn off some warnings for Flocq and Menhirlib +# These warnings can only be addressed upstream + +flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition +MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition extraction: extraction/STAMP |