diff options
| author | barras | 2004-01-14 16:52:06 +0000 |
|---|---|---|
| committer | barras | 2004-01-14 16:52:06 +0000 |
| commit | e92027584f4134f4fa89a77a752bf28aedd9c44a (patch) | |
| tree | 0eefd0cf15a2f05fed2f49bf8b1ff26796fdf834 /doc/Makefile | |
| parent | 4ba765fe88d88e5765d6058b7d366e03318b789a (diff) | |
ajout d'une passe de latex our avoir un index correct
+ quelques petites retouches sur la doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8476 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/doc/Makefile b/doc/Makefile index f338e3f57d..a0a50a6405 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -28,7 +28,7 @@ COQTOP=`$(DOCCOQC) -where` COQTEX=$(COQBINPATH)coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small #COQWEBSTY=$(HOME)/lib/tex/ COQWEBSTY=/usr/share/texmf/tex/latex/misc/ -HEVEALIB=/usr/local/lib/hevea +HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea LATEX=latex BIBTEX=bibtex -min-crossrefs=10 @@ -48,15 +48,16 @@ LIBFILES=library/Logic.tex library/Datatypes.tex library/Peano.tex \ REFMANCOQTEXFILES=\ RefMan-gal.v.tex RefMan-ext.v.tex RefMan-mod.v.tex RefMan-tac.v.tex \ RefMan-cic.v.tex RefMan-lib.v.tex RefMan-tacex.v.tex \ - RefMan-syn.v.tex RefMan-ltac.v.tex RefMan-oth.v.tex + RefMan-syn.v.tex RefMan-oth.v.tex COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex \ Omega.v.tex Changes.v.tex Tutorial.v.tex Polynom.v.tex \ - Correctness.v.tex Setoid.v.tex # Program.v.tex Natural.v.tex + Setoid.v.tex +#SUPPRIME: Program.v.tex Natural.v.tex Correctness.v.tex REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \ - RefMan-pro.tex RefMan-com.tex RefMan-uti.tex RefMan-ide.tex \ - coqide.eps coqide-queries.eps RefMan-add.tex RefMan-modr.tex \ + RefMan-pro.tex RefMan-com.tex RefMan-ltac.tex RefMan-uti.tex \ + RefMan-ide.tex coqide.eps coqide-queries.eps RefMan-add.tex RefMan-modr.tex \ $(REFMANCOQTEXFILES) REFMAN=Reference-Manual @@ -292,9 +293,12 @@ Tutorial.v.pdf: ./version.tex ./title.tex Tutorial.v.tex Reference-Manual.ps: Reference-Manual.dvi +# The second LATEX compilation is necessary otherwise the pages of the index +# are not correct (don't know why...) - BB Reference-Manual.dvi: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib $(LATEX) Reference-Manual $(BIBTEX) Reference-Manual + $(LATEX) Reference-Manual $(MAKEINDEX) Reference-Manual $(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind $(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind |