diff --git a/doc/.gitignore b/doc/.gitignore
index 068eb737..651eab93 100644
--- a/doc/.gitignore
+++ b/doc/.gitignore
@@ -1,25 +1,28 @@
+# Do not ignore these.  The release procedure (web-manual-update)
+# works in the src tree (even when run from the build tree) and leaves
+# these files around.  Since they take precedence over the files in
+# the build tree, locally built manuals use obsolete auxiliary files.
+#
+# So don't hide them, give the maintainer a chance to clean them.
+#/bison.aux
+#/bison.cp
+#/bison.cps
+#/bison.toc
+
 /*~
 /.dirstamp
 /bison.1
-/bison.aux
-/bison.cp
-/bison.cps
 /bison.dvi
-/bison.fn
 /bison.help
 /bison.html
 /bison.info
-/bison.ky
 /bison.log
 /bison.pdf
-/bison.pg
 /bison.ps
-/bison.toc
-/bison.tp
-/bison.vr
 /cross-options.texi
 /fdl.texi
 /gendocs_template
+/gendocs_template_min
 /gpl-3.0.texi
 /refcard.dvi
 /refcard.log
@@ -27,4 +30,3 @@
 /stamp-vti
 /version.texi
 /yacc.1
-/gendocs_template_min