aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2020-09-11 13:55:40 +0200
committerGitHub2020-09-11 13:55:40 +0200
commitbcbf0850d771c889431fb8d3c073c41059268c05 (patch)
treec21bcc2eaefe392975be94274b82e309a25cfa2d
parent4c35b309ece8c57088dffd7bea0ef7878f1d8d12 (diff)
Update mathcomp/Makefile.test-suite.coq.local
Co-authored-by: Erik Martin-Dorel <erik@martin-dorel.org>
-rw-r--r--mathcomp/Makefile.test-suite.coq.local6
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local
index 9db49c5..2de68fc 100644
--- a/mathcomp/Makefile.test-suite.coq.local
+++ b/mathcomp/Makefile.test-suite.coq.local
@@ -2,13 +2,13 @@ OUTPUT_TESTS=test_suite/output.v
OUTPUT_ARTIFACTS=$(OUTPUT_TESTS:%.v=%.v.out.new)
-COQ_VERSION=$(shell $(COQC) -print-version | cut -d ' ' -f 1 | cut -d '.' -f 1-2)
+COQ_VERSION_MINOR=$(shell $(COQC) -print-version | cut -d ' ' -f 1 | cut -d '.' -f 1-2)
# Given a file f we compare its compilation output f.out.new with
-# f.out.COQ_VERSION (or f.out if f.out.COQ_VERSION does not exist)
+# f.out.COQ_VERSION_MINOR (or f.out if f.out.COQ_VERSION_MINOR does not exist)
post-all:: $(OUTPUT_ARTIFACTS)
@for f in $(OUTPUT_TESTS); do\
- if [ -e $$f.out.$(COQ_VERSION) ]; then REFERENCE=$$f.out.$(COQ_VERSION);\
+ if [ -e "$$f.out.$(COQ_VERSION_MINOR)" ]; then REFERENCE="$$f.out.$(COQ_VERSION_MINOR)";\
else REFERENCE=$$f.out; fi;\
if ! diff -q "$$REFERENCE" "$$f.out.new"; \
then diff -u "$$REFERENCE" "$$f.out.new"; \