aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-01-13 17:21:21 +0000
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-09 12:14:16 +0100
commitf8cb1942284979bc7c325f2137fad1293380d855 (patch)
tree08e9e3ff7ac99c7c000bc4e0ca683a8e7eb677ea /Makefile.doc
parent7f207c26b603a40ecbb58377f6669935d0419366 (diff)
Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentation)
This commit r14895 comes apparently itself from commit r12010 in branch v8.2
Diffstat (limited to 'Makefile.doc')
-rw-r--r--Makefile.doc32
1 files changed, 12 insertions, 20 deletions
diff --git a/Makefile.doc b/Makefile.doc
index 7b8ade09e..bc6ae020b 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -133,7 +133,7 @@ refman-html-dir: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
(cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html)
$(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html
- $(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
+ -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
refman-quick:
(cd doc/refman;\
@@ -200,40 +200,32 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
### Standard library (browsable html format)
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 --utf8 \
- -R theories Coq $(THEORIESVO:.vo=.v)
- mv doc/stdlib/html/index.html doc/stdlib/index-body.html
+doc/stdlib/html/genindex.html:
else
-doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO)
+doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO)
+endif
- rm -rf doc/stdlib/html
$(MKDIR) doc/stdlib/html
- $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \
+ $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
-R theories Coq $(THEORIESVO:.vo=.v)
- mv doc/stdlib/html/index.html doc/stdlib/index-body.html
-endif
+ mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html
doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files
-doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html
- cat doc/stdlib/index-list.html > $@
- sed -n -e '/<table>/,/<\/table>/p' doc/stdlib/index-body.html >> $@
- cat doc/stdlib/index-trailer.html >> $@
+doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html
+ cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@
+ cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@
### Standard library (light version, full version is definitely too big)
ifdef QUICK
doc/stdlib/Library.coqdoc.tex:
- $(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 --utf8 \
- -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
+doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
endif
+ $(COQDOC) -q -boot --gallina --body-only --latex --stdout \
+ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
(cd doc/stdlib;\