travis-ci: record and skip successfully built trees

diff --git a/Documentation/Makefile b/Documentation/Makefile
index b5be2e2d3f5c8ade04fa81ddb5b24a8747838cdc..2415e0d6573e0dd9c0802708df1b5699d71dd09f 100644 (file)
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
@@ -31,6 +31,7 @@ MAN7_TXT += giteveryday.txt
 MAN7_TXT += gitglossary.txt
 MAN7_TXT += gitnamespaces.txt
 MAN7_TXT += gitrevisions.txt
+MAN7_TXT += gitsubmodules.txt
 MAN7_TXT += gittutorial-2.txt
 MAN7_TXT += gittutorial.txt
 MAN7_TXT += gitworkflows.txt