aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorMaxime Dénès2017-08-29 13:09:37 +0200
committerMaxime Dénès2017-08-29 13:09:37 +0200
commit799d17738ebbae30a007b308998a669a9139cf1d (patch)
tree9a10365b80b5320938c0a7ef1e6e392b49f52fb4 /test-suite
parentef0450ded84d0fc27b5051baf94acfb6e541a7bf (diff)
parentaf6a390219de9eb1a91ffd9f5ca15a2d2253e978 (diff)
Merge PR #985: Fix coqdoc test-suite target on Windows.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 1268ed14bc..78d90aad81 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -528,8 +528,8 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR
f=`basename $*`; \
$(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \
$(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \
- diff -u $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \
- grep -v "^%%" Coqdoc.$$f.tex | diff -u $$f.tex.out - 2>&1; S=$$?; times; \
+ diff -u --strip-trailing-cr $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \
+ grep -v "^%%" Coqdoc.$$f.tex | diff -u --strip-trailing-cr $$f.tex.out - 2>&1; S=$$?; times; \
if [ $$R = 0 -a $$S = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \