From 8d4d2f95d2b4d1ba1f7c1c4e5b5b9fbf6987ecfc Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 6 Dec 2024 15:44:58 +0100
Subject: [PATCH] Tweak the warning flags for extraction

---
 Makefile | 11 ++++++++++-
 test     |  2 +-
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 20947e842..0d4d24341 100644
--- a/Makefile
+++ b/Makefile
@@ -76,6 +76,15 @@ MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope
 flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
 MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
 
+# For the extraction phase, we silence other warnings:
+# change-dir-deprecated:
+#    warning introduced in 8.20, no alternative before 8.20
+# extraction-default-directory:
+#    warning introduced in 8.20, no alternative before 8.20
+COQEXTRACTOPTS ?= \
+  -w -change-dir-deprecated \
+  -w -extraction-default-directory
+
 ifneq ($(INSTALL_COQDEV),true)
 # Disable costly generation of .cmx files, which are not used locally
   COQCOPTS += -w -deprecated-native-compiler-option -native-compiler no
@@ -101,7 +110,7 @@ PROFILE_ZIP ?= true
 COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
 COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
 COQDOC="$(COQBIN)coqdoc"
-COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source
+COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) $(COQEXTRACTOPTS) -batch -load-vernac-source
 COQCHK="$(COQBIN)coqchk" $(COQINCLUDES)
 MENHIR=menhir
 CP=cp
diff --git a/test b/test
index 154895fe4..bbfd6c8f3 160000
--- a/test
+++ b/test
@@ -1 +1 @@
-Subproject commit 154895fe439c0ca50b60a711c30464509cd72f7f
+Subproject commit bbfd6c8f3de5d8e38988bd7f27af3a151e239bb4