diff --git a/ci/test-documentation.sh b/ci/test-documentation.sh index 6c018b673e..49f87f50fd 100755 --- a/ci/test-documentation.sh +++ b/ci/test-documentation.sh @@ -15,6 +15,13 @@ filter_log () { "$1" } +check_docs () { + test -s "$1"/Documentation/git.html && + test -s "$1"/Documentation/git.xml && + test -s "$1"/Documentation/git.1 && + grep " >(tee stdout.log) 2> >(tee stderr.raw >&2) cat stderr.raw filter_log stderr.raw >stderr.log test ! -s stderr.log -test -s Documentation/git.html -test -s Documentation/git.xml -test -s Documentation/git.1 -grep '