diff --git a/dodoc.sh b/dodoc.sh
index d6571ba7c6..a839bdab0b 100755
--- a/dodoc.sh
+++ b/dodoc.sh
@@ -72,7 +72,10 @@ make WEBDOC_DEST="$DOCREPO/doc-htmlpages" install-webdoc >../:html.log 2>&1 &&
 
 if test -d $PUBLIC
 then
-	make WEBDOC_DEST="$PUBLIC" install-webdoc >>../:html.log 2>&1
+	rm -f git.html &&
+	make WEBDOC_DEST="$PUBLIC" ASCIIDOC_EXTRA='-a stalenotes' \
+		install-webdoc >>../:html.log 2>&1 &&
+	rm -f git.html
 else
 	echo "* No public html at $PUBLIC"
 fi || exit $?