Merge branch 'jc/doc-git-updates'

diff --git a/Documentation/Makefile b/Documentation/Makefile
index 063fa696c9eff617e4fc6ad37f0b6e49d32d58f9..cf5916fe8b79e39eb57f97b36e82697694f41d7a 100644 (file)
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
@@ -344,4 +344,7 @@ require-htmlrepo::
 quick-install-html: require-htmlrepo
        '$(SHELL_PATH_SQ)' ./install-doc-quick.sh $(HTML_REPO) $(DESTDIR)$(htmldir)
 
+print-man1:
+       @for i in $(MAN1_TXT); do echo $$i; done
+
 .PHONY: FORCE