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 <vinc...@vinc17.net> - 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)
