From 4e83fd00bd97894338418db97121f267fa162608 Mon Sep 17 00:00:00 2001
From: Glenn Morris <rgm@gnu.org>
Date: Thu, 4 Mar 2021 10:44:07 -0800
Subject: [PATCH] * doc/misc/Makefile.in (echo-sources): New phony target.

---
 doc/misc/Makefile.in | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/doc/misc/Makefile.in b/doc/misc/Makefile.in
index ed33364440d..87d87bf2005 100644
--- a/doc/misc/Makefile.in
+++ b/doc/misc/Makefile.in
@@ -94,6 +94,15 @@ TEXI_FROM_ORG = ${ORG_SRC:.org=.texi}
 TARGETS_1 = $(INFO_INSTALL:ccmode=cc-mode)
 TARGETS = $(TARGETS_1:info.info=info)
 
+texi_sources = $(addsuffix .texi,${TARGETS})
+texi_notgen = $(filter-out $(notdir ${TEXI_FROM_ORG}),${texi_sources})
+texi_and_org = $(notdir ${ORG_SRC}) ${texi_notgen}
+SOURCES = $(sort ${texi_and_org})
+.PHONY: echo-sources
+## Used by the top-level Makefile.
+echo-sources:
+	@echo ${SOURCES}
+
 DVI_TARGETS  = $(TARGETS:=.dvi)
 HTML_TARGETS = $(TARGETS:=.html)
 PDF_TARGETS  = $(TARGETS:=.pdf)
-- 
2.39.2