diff options
| author | Théo Zimmermann | 2019-12-06 10:56:46 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-06 10:56:46 +0100 |
| commit | dff979d31a18dcf892fac75cd8a1e608adaefb9e (patch) | |
| tree | 72263d9853a21027792a8dea05ee54335dff3291 | |
| parent | f76a6a2444dbc80bfcb46c88449f62d76b6f4984 (diff) | |
| parent | dd413df1cc2fe27d89e2ef926200e53b50105dda (diff) | |
Merge PR #11232: Remove latex files that should be regenerated by make
Ack-by: Zimmi48
| -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) |