diff options
| author | Enrico Tassi | 2020-09-10 15:05:49 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-10 15:05:49 +0200 |
| commit | 8bfcb13c1576a8d6e55dc7c732ec3bda5f5e4f7d (patch) | |
| tree | e9b95bff0ee5becfa285ddd648d621780561ce0c /mathcomp | |
| parent | c0214cdb4a44261db539b48fb76dbdaded87312b (diff) | |
Update mathcomp/Makefile.test-suite.coq.local
Co-authored-by: Erik Martin-Dorel <erik@martin-dorel.org>
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/Makefile.test-suite.coq.local | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local index 5a1ec43..6f9454b 100644 --- a/mathcomp/Makefile.test-suite.coq.local +++ b/mathcomp/Makefile.test-suite.coq.local @@ -10,8 +10,7 @@ post-all:: $(OUTPUT_ARTIFACTS) @for f in $(OUTPUT_TESTS); do\ if [ -e $$f.out.$(COQ_VERSION) ]; then REFERENCE=$$f.out.$(COQ_VERSION);\ else REFERENCE=$$f.out; fi;\ - diff -u $$REFERENCE $$f.out.new > /dev/null;\ - if [ $$? -ne 0 ]; \ + if ! diff -q "$$REFERENCE" "$$f.out.new"; \ then echo "Output of file $$f differs!";\ diff -u $$REFERENCE $$f.out.new;\ exit 1;\ @@ -19,4 +18,4 @@ post-all:: $(OUTPUT_ARTIFACTS) done $(OUTPUT_ARTIFACTS): %.v.out.new: %.v all/all.vo - $(COQC) $(COQFLAGS) $(COQLIBS) $< > $<.out.new
\ No newline at end of file + $(COQC) $(COQFLAGS) $(COQLIBS) $< > $<.out.new |