fix-coqmakefile.patch

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index c9795ef2b4..38ac149477 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -592,13 +592,18 @@ beautify: $(BEAUTYFILES)
 # There rules can be extended in @LOCAL_FILE@
 # Extensions can't assume when they run.
 
+.filestoinstall:
+	@:$(if $(HASFILE),$(file >$@,$(FILESTOINSTALL)),\
+	    $(shell rm -f $@) \
+	    $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> $@)))
+
 # findlib needs the package to not be installed, so we remove it before
 # installing it (see the call to findlib_remove)
-install: META
-	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
+install: META .filestoinstall
+	$(HIDE)code=0; for f in $$(cat .filestoinstall); do\
 	 if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
 	done; exit $$code
-	$(HIDE)for f in $(FILESTOINSTALL); do\
+	$(HIDE)for f in $$(cat .filestoinstall); do\
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
 	 if [ "$$?" != "0" -o -z "$$df" ]; then\
 	   echo SKIP "$$f" since it has no logical path;\
@@ -640,16 +645,16 @@ install-doc:: html mlihtml
 	done
 .PHONY: install-doc
 
-uninstall::
+uninstall:: .filestoinstall
 	@# Extension point
 	$(call findlib_remove)
-	$(HIDE)for f in $(FILESTOINSTALL); do \
+	$(HIDE)for f in $$(cat .filestoinstall); do \
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
 	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
 	 echo RM "$$instf" ;\
 	done
-	$(HIDE)for f in $(FILESTOINSTALL); do \
+	$(HIDE)for f in $$(cat .filestoinstall); do \
 	 df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
 	 echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\
 	 (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \