diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 14:30:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-13 23:33:41 +0100 |
| commit | f5c995467f8342e84bd73ac6d6bbd3c3281b2b4e (patch) | |
| tree | 8eb227295d49de0ec60a4c17c07d5447f99b71e6 /test-suite/Makefile | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
Fixing encoding in coqdoc output tests.
The file links.v is using utf-8 characters so this is needed at least
to test this file. For the other files, it is not completely without
effect since it makes that symbols like => and forall are respectively
displayed ⇒ and ∀.
Maybe tests with iso-8859-1 or test without a charset option should be
kept.
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 61e75fa5d..7a204bfd8 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -549,8 +549,8 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR $(coqc) -R coqdoc Coqdoc $* 2>&1; \ cd coqdoc; \ 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; \ + $(coqdoc) -utf8 -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ + $(coqdoc) -utf8 -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ 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 \ |