diff options
| author | Jim Fehrle | 2019-12-02 16:02:31 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-12-02 16:02:31 -0800 |
| commit | dd413df1cc2fe27d89e2ef926200e53b50105dda (patch) | |
| tree | b1c5bbe047c1226296777f9a6a5d82e0ed51109e | |
| parent | 79bbca336a226693770e37db3a8f05b2819acb5c (diff) | |
Remove latex files that should be regenerated by make
If these files are present in the latex directory, "make refman-pdf"
may fail to generate CoqRefMan.pdf.
| -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) |