Don't fflush(stdout) when it's not helpful

diff --git a/Documentation/Makefile b/Documentation/Makefile
index cc563247a9faf54a8a6458ec0359620764fa3b9d..f3a6c733b662f4e9d06bc69cadc2201ea34f41ce 100644 (file)
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
@@ -29,7 +29,7 @@ DOC_MAN7=$(patsubst %.txt,%.7,$(MAN7_TXT))
 
 prefix?=$(HOME)
 bindir?=$(prefix)/bin
-mandir?=$(prefix)/man
+mandir?=$(prefix)/share/man
 man1dir=$(mandir)/man1
 man5dir=$(mandir)/man5
 man7dir=$(mandir)/man7