diff options
Diffstat (limited to 'Makefile.doc')
-rw-r--r-- | Makefile.doc | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/Makefile.doc b/Makefile.doc index 2190ebf69..cf849dadf 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -45,11 +45,11 @@ rectutorial: doc/RecTutorial/RecTutorial.html \ ### Implicit rules ###################################################################### -ifeq ($(QUICK),1) +ifdef QUICK %.v.tex: %.tex (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) else -%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(CONTRIBCMO) $(THEORIESVO) +%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(THEORIESVO) (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) endif @@ -87,7 +87,7 @@ doc/common/version.tex: config/Makefile # The second LATEX compilation is necessary otherwise the pages of the index # are not correct (don't know why...) - BB -doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Reference-Manual.tex +doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex @(cd doc/refman;\ $(LATEX) -interaction=batchmode Reference-Manual;\ $(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\ @@ -102,7 +102,7 @@ doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Referenc $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ - ../tools/show_latex_messages -no-overfull Reference-Manual.log) + ../tools/show_latex_messages -no-overfull Reference-Manual.log) doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex (cd doc/refman;\ @@ -185,7 +185,7 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) -ifeq ($(QUICK),1) +ifdef QUICK doc/stdlib/index-body.html: - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html @@ -211,7 +211,7 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm ### Standard library (light version, full version is definitely too big) -ifeq ($(QUICK),1) +ifdef QUICK doc/stdlib/Library.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ @@ -292,3 +292,9 @@ install-doc-printable: $(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps $(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps + + +# For emacs: +# Local Variables: +# mode: makefile +# End: |