On Mon, May 15, 2023 at 12:33:17PM +0200, Alvaro Herrera wrote:
> But make_ctags is *our* script, so I think this rule applies to them as
> well. (In any case, what can be hurt? We're not going to add any files
> to git named "tags" anyway.)
Yes, you have a point about the origin of the script generating the
tags. One thing is that one can still add a file even if listed in
what to ignore, as long as it is done with git-add -f. Okay, that's
not going to happen.
(FWIW, looking at my stuff, I have just set up that globally in 2018
after seeing the other thread.)
--
Michael