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.