On Sun, Sep 24, 2023 at 07:14:53PM +0200, Grégory Vanuxem wrote:
> Hello,
>
> I'm setting up a new more general Git management environment on my
> machine and looking at the FriCAS vanilla .gitignore file, I allowed
> myself to send here a diff with the one I use. I just did two
> additions today to the one I use. It could be of interest even if some
> stuff will not suit all needs.
To say the truth, I would prefer to keep .gitignore as small as
possible. IIUC .gitignore plays role when commiting changes.
At that time git remainds about possibly forgotten files.
When using separate build directory there should be almost
no trash in repository, so not much need to ignore things.
OTOH too wide ignore pattern may lead to missing files during
commit.
--
Waldek Hebisch