diff options
| author | Glenn Morris <rgm@gnu.org> | 2021-03-04 10:44:07 -0800 |
|---|---|---|
| committer | Glenn Morris <rgm@gnu.org> | 2021-03-04 10:44:07 -0800 |
| commit | 4e83fd00bd97894338418db97121f267fa162608 (patch) | |
| tree | f6f37ca3de5b302c2f11d250f1efaba44b6fd0f2 /doc/misc/Makefile.in | |
| parent | bd443f4e9c50463524f48cf5c43f35f2cecd528a (diff) | |
| download | emacs-4e83fd00bd97894338418db97121f267fa162608.tar.gz | |
* doc/misc/Makefile.in (echo-sources): New phony target.
Diffstat (limited to 'doc/misc/Makefile.in')
| -rw-r--r-- | doc/misc/Makefile.in | 9 |
1 files changed, 9 insertions, 0 deletions
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) |