aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-29 17:05:59 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-29 17:05:59 +0000
commit65fe36d2ad32f2c46c67369555aa5f3461570b78 (patch)
tree75673616a4ad43394696cda74c2a6f67b564c86a /Makefile.doc
parent627ab72099948f785920b5bc863cc9f5e9d9ad11 (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.doc5
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