git: don't ignore auxiliary Texinfo files

As a matter of fact, I think it is wrong to gitignore generated files
that belong to the build tree.  There should be the strict minimum,
and it's up to people that build in place to adjust their own
~/.gitignore.

* doc/.gitignore: here.
Remove files we no longer produce (thanks to texi2dvi).

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