bug#76530: closed (Remove or update dir file in the debbugs package)

[GNU bug Tracking System]

Your message dated Tue, 11 Mar 2025 10:36:18 +0100
with message-id <87frjjq57x.fsf@gmx.de>
and subject line Re: bug#76530: Remove or update dir file in the debbugs package
has caused the debbugs.gnu.org bug report #76530,
regarding Remove or update dir file in the debbugs package
to be marked as done.

(If you believe you have received this mail in error, please contact
help-debbugs@gnu.org.)


-- 
76530: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=76530
GNU Bug Tracking System
Contact help-debbugs@gnu.org with problems
> --- Begin Message ---
>
>
>
> Subject: 
>
> Remove or update dir file in the debbugs package
>
>
>
>
> Date: 
>
> Mon, 24 Feb 2025 21:04:48 +0100
>
>
>
>
> The last commit changed the $direntry name of the manuals, but the
> tracked dir file was not updated.  Because that file is being tracked,
> running install-info results in uncommitted changes.
>
> I recommend you remove this file; I believe it is not commonly tracked.
>
> Alternatively regenerate it and check in the changes.  I would have done
> that myself, but this resulted in more changes than what one would
> expect from looking just at 69f4dc14e8cbffbada422fe4e2d5640692a63425.
> It appears it makes a difference what version of install-info is used --
> another reason not to check in this file.
>
>     Cheers,
>     Jonas
>
>
>
> --- End Message ---
> --- Begin Message ---
>
>
>
> Subject: 
>
> Re: bug#76530: Remove or update dir file in the debbugs package
>
>
>
>
> Date: 
>
> Tue, 11 Mar 2025 10:36:18 +0100
>
>
>
>
> User-agent: 
>
> Gnus/5.13 (Gnus v5.13)
>
>
>
>
> Michael Albinus <michael.albinus@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.
>
> If you need it it locally in git, Makefile is your friend. Call 'make doc'.
>
> Closing the bug.
>
> >>     Cheers,
> >>     Jonas
>
> Best regards, Michael.
>
>
> --- End Message ---