Subject: bug#54365: the .gitignore file is modified

From: Vincent Lefevre <[email-masked]>
Date: Sun, 13 Mar 2022 02:41:45 +0100

The .gitignore file is modified as follows, possibly by the
bootstrap script:

diff --git a/.gitignore b/.gitignore
index 6735488..5b1afa6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
+/build-aux
 *.a
 *.exe
 *.o

The .gitignore file already has "/build-aux/", so that the above
change is probably incorrect.

-- 
Vincent Lefèvre <[email-masked]> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)