Subject: Re: bug#76530: Remove or update dir file in the debbugs package
From: Michael Albinus <[email-masked]>
To: [email-masked]
Cc: [email-masked], Stefan Monnier <[email-masked]>
Date: Tue, 11 Mar 2025 10:36:18 +0100
List-Id: <debbugs-submit.debbugs.gnu.org>

Michael Albinus <[email-masked]> 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.

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

Closing the bug.

>>     Cheers,
>>     Jonas

Best regards, Michael.