gforth
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: turn off history


From: Anton Ertl
Subject: Re: turn off history
Date: Wed, 27 Jul 2022 13:13:08 +0200

On Wed, Jul 27, 2022 at 01:00:37PM +0200, Bernd Paysan wrote:
> Another question is: Should we open the history file later in the boot 
> process, 
> e.g. on entering interactive mode?  There's no need to do that earlier.

I have been thinking about having a word INTERACTIVE-COLD or somesuch,
used like 'COLD, but only invoked when enterin interactive mode, but
have not acted (yet).

- anton





reply via email to

[Prev in Thread] Current Thread [Next in Thread]