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 '