diff --git a/src/scripts/doc/docbook.sh b/src/scripts/doc/docbook.sh
index 32c1a05..520e7b7 100755
--- a/src/scripts/doc/docbook.sh
+++ b/src/scripts/doc/docbook.sh
@@ -175,7 +175,7 @@ while [ $# -gt 0 ]; do
 			source="${target#$OBJDIR}"
 			source="${source%.*}.xml"
 			xpath="string(/refentry/refmeta/manvolnum)"
-			section=$($XMLLINT --xpath "$xpath" "$source")
+			section=$($DEBUG $XMLLINT --xpath "$xpath" "$source")
 			if [ $? -eq 0 -a -n "$section" ]; then
 				instdir="$MANDIR/html$section"
 			fi