From c0df11e0c7495aa2e48bc4440eb1c4e844f4857d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Mar 2023 09:56:58 +0100 Subject: 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. --- Makefile | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index e71dde6c..1a468acf 100644 --- a/Makefile +++ b/Makefile @@ -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 -- cgit