From d297a43246fafad4f1dccd04160fc1b85fea4e19 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 11 Sep 2024 18:55:08 +0200 Subject: [PATCH] move COQ_REF further up so it is easier to see --- Makefile.coq.local | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Makefile.coq.local b/Makefile.coq.local index 59bd0926..cb755ccd 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -4,6 +4,11 @@ NO_TEST:= # use MAKE_REF=1 to generate new reference files MAKE_REF:= +# Only test reference output on known versions of Coq, to avoid blocking +# Coq CI when they change the printing a little. +# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later. +COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1) + # Run tests interleaved with main build. They have to be in the same target for this. real-all: style $(if $(NO_TEST),,test) @@ -24,10 +29,6 @@ test: $(TESTFILES:.v=.vo) .PHONY: test COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode -# Only test reference output on known versions of Coq, to avoid blocking -# Coq CI when they change the printing a little. -# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later. -COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1) tests/.coqdeps.d: $(TESTFILES) $(SHOW)'COQDEP TESTFILES' -- GitLab