diff options
Diffstat (limited to 'doc/misc/Makefile.in')
| -rw-r--r-- | doc/misc/Makefile.in | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/misc/Makefile.in b/doc/misc/Makefile.in index 7982c0dc5ae..8be84e3fad1 100644 --- a/doc/misc/Makefile.in +++ b/doc/misc/Makefile.in @@ -130,12 +130,12 @@ info: $(INFO_TARGETS) ## Used by top-level Makefile. ## Base file names of output info files. +INFO_BASES = $(patsubst %.info,%,$(notdir $(INFO_INSTALL))) echo-info: - @echo "$(INFO_INSTALL) " | \ - sed -e 's|[^ ]*/||g' -e 's/\.info//g' -e "s/ */.info /g" + @: $(info $(addsuffix .info,$(INFO_BASES))) echo-sources: - @echo ${SOURCES} + @: $(info $(SOURCES)) dvi: $(DVI_TARGETS) |