diff options
| -rw-r--r-- | doc/misc/Makefile.in | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/misc/Makefile.in b/doc/misc/Makefile.in index ed1c497c25e..83bc2d7bf33 100644 --- a/doc/misc/Makefile.in +++ b/doc/misc/Makefile.in @@ -215,12 +215,13 @@ mkinfodir = @cd ${srcdir}; test -d ${infodir} || mkdir ${infodir} || test -d ${i .PHONY: info dvi pdf echo-info +# Default. +info: $(INFO_TARGETS) + ## Used by top-level Makefile. echo-info: @echo $(INFO_TARGETS) | sed 's|[^ ]*/||g' -info: $(INFO_TARGETS) - # please modify this for all the web manual targets webhack: clean $(MAKE) pdf MAKEINFO_OPTS="-DWEBHACKDEVEL $(MAKEINFO_OPTS)" |