Re: Using make_ctags leaves tags files in git

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