diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index cf849dadf..e5822eb5b 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -49,7 +49,7 @@ ifdef QUICK %.v.tex: %.tex (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) else -%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(THEORIESVO) +%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO) (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) endif |