diff options
| -rw-r--r-- | Makefile.doc | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile.doc b/Makefile.doc index 8e958532f0..125a4b33d5 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -71,7 +71,10 @@ refman-%: $(SPHINX_DEPS) doc/unreleased.rst $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* +COQREFMAN_FILES := $(wildcard $(SPHINXBUILDDIR)/latex/CoqRefMan*) +LATEX_REMOVE_FILES := $(filter-out $(SPHINXBUILDDIR)/latex/CoqRefMan.tex, $(COQREFMAN_FILES)) refman-pdf: refman-latex + rm -f $(LATEX_REMOVE_FILES) +$(MAKE) -C $(SPHINXBUILDDIR)/latex refman: $(SPHINX_DEPS) |