diff options
| author | Enrico Tassi | 2020-09-10 15:06:07 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-10 15:06:07 +0200 |
| commit | 18edef73cdf0fb6671dbfb2e9d5829182a065919 (patch) | |
| tree | 5a9e9b48363430bfef092c5427e7dc26dffce00c /mathcomp | |
| parent | 8bfcb13c1576a8d6e55dc7c732ec3bda5f5e4f7d (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 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local index 6f9454b..119eff1 100644 --- a/mathcomp/Makefile.test-suite.coq.local +++ b/mathcomp/Makefile.test-suite.coq.local @@ -11,8 +11,7 @@ post-all:: $(OUTPUT_ARTIFACTS) if [ -e $$f.out.$(COQ_VERSION) ]; then REFERENCE=$$f.out.$(COQ_VERSION);\ else REFERENCE=$$f.out; fi;\ if ! diff -q "$$REFERENCE" "$$f.out.new"; \ - then echo "Output of file $$f differs!";\ - diff -u $$REFERENCE $$f.out.new;\ + then diff -u "$$REFERENCE" "$$f.out.new"; \ exit 1;\ fi;\ done |