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: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: Michael Albinus <michael.albinus <at> gmx.de>
Cc: tracker <at> debbugs.gnu.org
Subject: bug#76530: closed (Remove or update dir file in the debbugs package)
Date: Tue, 11 Mar 2025 09:37:02 +0000

[Message part 1 (text/plain, inline)]

Your message dated Tue, 11 Mar 2025 10:36:18 +0100
with message-id <87frjjq57x.fsf <at> 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 <at> gnu.org.)


-- 
76530: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=76530
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

From: Jonas Bernoulli <jonas <at> bernoul.li>
To: bug-gnu-emacs <at> gnu.org
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

[Message part 3 (message/rfc822, inline)]

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

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.

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

Closing the bug.

>>     Cheers,
>>     Jonas

Best regards, Michael.

Previous Next

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