git: don't ignore auxiliary Texinfo files

[Akim Demaille]

commit 545fbc6c618915734777dbdaa2d9e44201a6515c
Author: Akim Demaille <address@hidden>
Date:   Sat Oct 20 08:18:34 2018 +0200

    git: don't ignore auxiliary Texinfo files
    
    As a matter of fact, I think it is wrong to put generated files that
    belong to the build tree here.  There should be the strict minimum,
    and it's up to people that build in place to adjust their own
    ~/.gitignore.
    
    * doc/.gitignore: here.

diff --git a/doc/.gitignore b/doc/.gitignore
index 068eb737..fc559e79 100644
--- a/doc/.gitignore
+++ b/doc/.gitignore
@@ -1,9 +1,15 @@
+# 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.
+#/bison.aux
+#/bison.cp
+#/bison.cps
+#/bison.toc
+
 /*~
 /.dirstamp
 /bison.1
-/bison.aux
-/bison.cp
-/bison.cps
 /bison.dvi
 /bison.fn
 /bison.help
@@ -14,12 +20,12 @@
 /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 +33,3 @@
 /stamp-vti
 /version.texi
 /yacc.1
-/gendocs_template_min