Merge branch 'da/difftool'

diff --git a/Documentation/Makefile b/Documentation/Makefile
index 3e39e2815baca82fe5f1fff8791de37c3c7247ac..f6e288bc634cc9a7b231cac0a237a7770efd098f 100644 (file)
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
@@ -204,6 +204,7 @@ ifndef V
        QUIET_DBLATEX   = @echo '   ' DBLATEX $@;
        QUIET_XSLTPROC  = @echo '   ' XSLTPROC $@;
        QUIET_GEN       = @echo '   ' GEN $@;
+       QUIET_LINT      = @echo '   ' LINT $@;
        QUIET_STDERR    = 2> /dev/null
        QUIET_SUBDIR0   = +@subdir=
        QUIET_SUBDIR1   = ;$(NO_SUBDIR) echo '   ' SUBDIR $$subdir; \
@@ -427,4 +428,7 @@ quick-install-html: require-htmlrepo
 print-man1:
        @for i in $(MAN1_TXT); do echo $$i; done
 
+lint-docs::
+       $(QUIET_LINT)$(PERL_PATH) lint-gitlink.perl
+
 .PHONY: FORCE