From dd413df1cc2fe27d89e2ef926200e53b50105dda Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 2 Dec 2019 16:02:31 -0800
Subject: 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.
---
 Makefile.doc | 3 +++
 1 file changed, 3 insertions(+)

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)
-- 
cgit v1.2.3