diff options
| author | Enrico Tassi | 2020-09-11 13:55:40 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-11 13:55:40 +0200 |
| commit | bcbf0850d771c889431fb8d3c073c41059268c05 (patch) | |
| tree | c21bcc2eaefe392975be94274b82e309a25cfa2d /mathcomp/Makefile.test-suite.coq.local | |
| parent | 4c35b309ece8c57088dffd7bea0ef7878f1d8d12 (diff) | |
Update mathcomp/Makefile.test-suite.coq.local
Co-authored-by: Erik Martin-Dorel <erik@martin-dorel.org>
Diffstat (limited to 'mathcomp/Makefile.test-suite.coq.local')
| -rw-r--r-- | mathcomp/Makefile.test-suite.coq.local | 6 |
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"; \ |