diff --git a/Makefile.rules b/Makefile.rules index 26373272cc..35403d51bf 100644 --- 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 index d3708003c2..d15f04bdce 100644 --- 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 index 30c1cf762f..009b241ce5 100644 --- a/etc/ci.sh +++ b/etc/ci.sh @@ -127,6 +127,7 @@ GAPInput makemanuals) make doc + make check-manuals ;; testmanuals)