diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-08-21 15:30:48 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-08-21 15:30:48 +0200 |
| commit | 7db02b704b9b99e364d23f5ac4ed24594a31f88e (patch) | |
| tree | 20c11e6d69a6a588956b528546f08988c640bb97 /test-suite/Makefile | |
| parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) | |
Fix coqdoc test-suite target on Windows.
Commit 8f12597 introduced new output tests but these were broken on Windows.
We fix them by using --strip-trailing-cr option of diff, like in other
output tests in the test-suite.
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 1268ed14b..78d90aad8 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"; \ |