aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.doc')
-rw-r--r--Makefile.doc18
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: