GNU bug report logs - #76530
Remove or update dir file in the debbugs package

Previous Next

Full log

View this message in rfc822 format

From: Jonas Bernoulli <jonas <at> bernoul.li>
To: Michael Albinus <michael.albinus <at> gmx.de>, 76530-done <at> debbugs.gnu.org
Cc: Stefan Monnier <monnier <at> iro.umontreal.ca>
Subject: bug#76530: Remove or update dir file in the debbugs package
Date: Tue, 11 Mar 2025 13:52:56 +0100

Michael Albinus <michael.albinus <at> gmx.de> writes:

> Michael Albinus <michael.albinus <at> gmx.de> writes:
>
> Hi Jonas,
>
>>> I recommend you remove this file; I believe it is not commonly tracked.
>>
>> (package-initialize) adds the directories, where packages are installed,
>> to Info-directory-list. Therefore, the dir file is taken into account.
>
> Finally, I've removed the dir file from git, as recommended by Stefan
> Monnier. It is generated automatically when creating a package release.

Thanks!

> If you need it it locally in git, Makefile is your friend. Call 'make doc'.

I'm already friends with the Makefile.  ;)

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.