From 4d90c1983907ff3ea8a5a8c4dca1dba57c5bf3f8 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 28 Sep 2009 15:04:07 +0000 Subject: Fix the stdlib doc compilation + switch all .v file to utf8 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.doc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'Makefile.doc') diff --git a/Makefile.doc b/Makefile.doc index 3da6e10b8..49b377ef7 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -189,14 +189,14 @@ ifdef QUICK doc/stdlib/index-body.html: - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \ + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html else doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO) - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \ + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html endif @@ -213,11 +213,11 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm ifdef QUICK doc/stdlib/Library.coqdoc.tex: - $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ else doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO) - $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ endif -- cgit v1.2.3