diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-29 17:05:59 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-29 17:05:59 +0000 |
commit | 65fe36d2ad32f2c46c67369555aa5f3461570b78 (patch) | |
tree | 75673616a4ad43394696cda74c2a6f67b564c86a /Makefile.doc | |
parent | 627ab72099948f785920b5bc863cc9f5e9d9ad11 (diff) |
Solves some warning and hides some not-bad ones in doc. It remains a
few hevea warning (failure to put a vector on an expression in
Classes.tex, failure to support multirow in RecTutorial.tex).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11868 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.doc')
-rw-r--r-- | Makefile.doc | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index 9382e1b6f..5a02817e5 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -66,6 +66,9 @@ endif HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file" SHOWMAKEINDEXERROR=egrep "^!! Input index error|^** Input style error|^ --" +# Empty subsection levels in faq are on purpose +HEVEAFAQFILTER=|& grep -v "^Warning: List with no item" + ###################################################################### # Common ###################################################################### @@ -162,7 +165,7 @@ doc/faq/FAQ.v.pdf: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.dvi ../tools/show_latex_messages FAQ.v.log) doc/faq/FAQ.v.html: doc/faq/FAQ.v.dvi # to ensure FAQ.v.bbl - (cd doc/faq; $(HEVEA) $(HEVEAOPTS) FAQ.v.tex) + (cd doc/faq; ($(HEVEA) $(HEVEAOPTS) FAQ.v.tex $(HEVEAFAQFILTER))) doc/faq/html/index.html: doc/faq/FAQ.v.html - rm -rf doc/faq/html |