From bfbd73f3e0ee866e2fbd9fe8a63f72dd3b9bcafc Mon Sep 17 00:00:00 2001
From: Akim Demaille <akim.demaille@gmail.com>
Date: Sat, 20 Oct 2018 08:18:34 +0200
Subject: [PATCH] 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 | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

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