On Mon, Feb 06, 2023 at 03:40:44PM +0100, Peter Krempa wrote:
On Mon, Feb 06, 2023 at 15:38:11 +0100, Martin Kletzander wrote:
> On Mon, Feb 06, 2023 at 03:32:20PM +0100, Peter Krempa wrote:
> > On Mon, Feb 06, 2023 at 15:28:29 +0100, Martin Kletzander wrote:
> > > This reverts commit f2d379e7cb802f922409c35e4831ee52a2162486. On top of
that it
> > > also removes the `/tags` file because we don't even have the `make
tags` target
> > > any more. Any tool-related ignores should go to user's global ignore
file or
> > > the user's local exclude file which is per-project. See git-config(1)
and
> > > gitignore(5) for more details.
> >
> > We still carry '.ctags'. With that directory you don't need any
fancy
> > 'make tags' because simply running 'ctags' in the source code
directory
> > just does the right thing.
> >
>
> So /tags it's not needed in the .gitignore either.
I don't quite follow why. Running 'ctags' with the configuration we have
in the repository creates an untracked 'tags' file which we don't want
to commit/distribute.
Oh, and that creates the tags file, I misunderstood the first comment
then, I'll remove the removal of /tags from the commit then.