GNU bug report logs - #38308
INFO files changed on disk: mention rereading workaround

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 38308 in the body.
You can then email your comments to 38308 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: 積丹尼 Dan Jacobson <jidanni <at> jidanni.org>
To: bug-gnu-emacs <at> gnu.org
Subject: INFO files changed on disk: mention rereading workaround
Date: Thu, 21 Nov 2019 08:11:26 +0800

(info "(info) Advanced") should add FAQ:

Q: What if the info files or top directory change on disk?  Unlike
normal browsers INFO has no refresh command.

A: Kill the *info* buffer and start INFO again.

Message #8 received at 38308 <at> debbugs.gnu.org (full text, mbox):

From: Robert Pluim <rpluim <at> gmail.com>
To: 積丹尼 Dan Jacobson <jidanni <at> jidanni.org>
Cc: 38308 <at> debbugs.gnu.org
Subject: Re: bug#38308: INFO files changed on disk: mention rereading
 workaround
Date: Thu, 21 Nov 2019 09:14:31 +0100

>>>>> On Thu, 21 Nov 2019 08:11:26 +0800, 積丹尼 Dan Jacobson <jidanni <at> jidanni.org> said:

    積丹尼> (info "(info) Advanced") should add FAQ:
    積丹尼> Q: What if the info files or top directory change on disk?  Unlike
    積丹尼> normal browsers INFO has no refresh command.

    積丹尼> A: Kill the *info* buffer and start INFO again.

You donʼt have to kill the *info* buffer, you can just revert it. I do
that all the time when Iʼm writing info documentation, but I canʼt see
that being a common occurence in normal use.

Robert

Message #11 received at 38308 <at> debbugs.gnu.org (full text, mbox):

From: Lars Ingebrigtsen <larsi <at> gnus.org>
To: Robert Pluim <rpluim <at> gmail.com>
Cc: 38308 <at> debbugs.gnu.org,
 積丹尼 Dan Jacobson <jidanni <at> jidanni.org>
Subject: Re: bug#38308: INFO files changed on disk: mention rereading
 workaround
Date: Thu, 21 Nov 2019 14:04:09 +0100

Robert Pluim <rpluim <at> gmail.com> writes:

>>>>>> On Thu, 21 Nov 2019 08:11:26 +0800, 積丹尼 Dan Jacobson
> <jidanni <at> jidanni.org> said:
>
>     積丹尼> (info "(info) Advanced") should add FAQ:
>     積丹尼> Q: What if the info files or top directory change on disk?  Unlike
>     積丹尼> normal browsers INFO has no refresh command.
>
>     積丹尼> A: Kill the *info* buffer and start INFO again.
>
> You donʼt have to kill the *info* buffer, you can just revert it. I do
> that all the time when Iʼm writing info documentation, but I canʼt see
> that being a common occurence in normal use.

Yeah, I don't think this is a frequently asked question, so I'm closing
this bug report.

-- 
(domestic pets only, the antidote for overdose, milk.)
   bloggy blog: http://lars.ingebrigtsen.no

Message #18 received at 38308 <at> debbugs.gnu.org (full text, mbox):

From: 積丹尼 Dan Jacobson <jidanni <at> jidanni.org>
To: Lars Ingebrigtsen <larsi <at> gnus.org>
Cc: Robert Pluim <rpluim <at> gmail.com>, 38308 <at> debbugs.gnu.org
Subject: Re: bug#38308: INFO files changed on disk: mention rereading
 workaround
Date: Thu, 21 Nov 2019 23:00:22 +0800

Dired says the file changed on disk, use g to...

Info doesn't.

Therefore dired shouldn't either.

Or info should at least add *one little itty bitty word* in its
documentation about the issue.

Previous Next

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