From 2b3d84dcd68425b7106a49fa390aa25b89e5f3a9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 5 Aug 2026 18:08:05 +0000 Subject: [PATCH] Makefile: use an explicit path for extraction/extraction.v An implicit relative path passed to -load-vernac-source is looked up in the load path, so an installed package with an "extraction" subdirectory shadows CompCert's own extraction.v. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 469380c15..b862173b8 100644 --- a/Makefile +++ b/Makefile @@ -282,7 +282,7 @@ extraction: extraction/STAMP extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMachdep.v rm -f extraction/*.ml extraction/*.mli - $(COQEXEC) extraction/extraction.v + $(COQEXEC) ./extraction/extraction.v @if grep 'AXIOM TO BE REALIZED' extraction/*.ml; then \ echo "An error occured during extraction to OCaml code."; \ echo "Check the versions of Flocq and MenhirLib used."; \