diff options
Diffstat (limited to 'Makefile.in')
| -rw-r--r-- | Makefile.in | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/Makefile.in b/Makefile.in index 7b271f12424..4cdd293ebd4 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1043,11 +1043,9 @@ uninstall-ps: $(UNINSTALL_PS) # and it's not worth it. This case is only relevant if you download a # release, then change the .texi files. info: - @if test "$(HAVE_MAKEINFO)" = "no"; then \ - echo "Configured --without-makeinfo, not building manuals" ; \ - else \ - $(MAKE) info-real info-dir; \ - fi + ifneq ($(HAVE_MAKEINFO),no) + $(MAKE) info-real info-dir + endif ## build-aux/make-info-dir expects only certain dircategories. check-info: info |