[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

git: don't ignore auxiliary Texinfo files

From: Akim Demaille
Subject: git: don't ignore auxiliary Texinfo files
Date: Sat, 20 Oct 2018 14:07:26 +0200

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
    * 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.
@@ -14,12 +20,12 @@
@@ -27,4 +33,3 @@

reply via email to

[Prev in Thread] Current Thread [Next in Thread]