Add make check-manuals to makemanuals Travis test

ssiccha · Mar 27, 2019 · ebe0d6f · ebe0d6f
1 parent 33f97dd
commit ebe0d6f
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/Makefile.rules b/Makefile.rules
@@ -754,9 +754,8 @@ clean-doc:
 # Manual consistency check
 check-manuals: all
 	$(MKDIR_P) dev/log
-	((cd doc/ref ; \
-	  echo 'Read("testconsistency.g");' | $(TESTGAP) ) \
-	  > `date -u +dev/log/check_manuals_%Y-%m-%d-%H-%M` 2>&1 )
+	( cd doc/ref ; echo 'Read("testconsistency.g");' | $(TESTGAP) | \
+	               tee `date -u +../../dev/log/check_manuals_%Y-%m-%d-%H-%M` )
 
 .PHONY: doc clean-doc manuals check-manuals
 

diff --git a/doc/ref/testconsistency.g b/doc/ref/testconsistency.g
@@ -238,7 +238,8 @@ Print( with, " with examples \n");
 Print( without , " without examples \n");
 end;
 
-CheckDocCoverage(doc);
+# Uncomment next line to add ManSections without examples to the test log
+# CheckDocCoverage(doc);
 QUIT_GAP( CheckManSectionTypes(doc) );
 
 
diff --git a/etc/ci.sh b/etc/ci.sh
@@ -127,6 +127,7 @@ GAPInput
 
   makemanuals)
     make doc
+    make check-manuals
     ;;
 
   testmanuals)