diff --git a/lib/modules/Tools.pmod/Standalone.pmod/git_export_autodoc.pike b/lib/modules/Tools.pmod/Standalone.pmod/git_export_autodoc.pike
index fdc4e895ccf4207fbb233a1cae254090eabf6db9..f2d942d5eb10568a5a11c1eeaa188cebeb9e573f 100644
--- a/lib/modules/Tools.pmod/Standalone.pmod/git_export_autodoc.pike
+++ b/lib/modules/Tools.pmod/Standalone.pmod/git_export_autodoc.pike
@@ -720,7 +720,9 @@ void export_autodoc_for_ref(string ref)
     {
         // Not relevant for autodoc.
         src_to_doc[src_rev] = doc_refs[ref];
-        progress("no documentation... ");
+	if (verbose) {
+            progress("No documentation... ");
+	}
         continue;
     }