On Sat, Nov 30, 2024, at 9:36 PM, Dan Jacobson wrote:
> We see for simple
> $ history
> output, there's no way to change the file it reads, at least with the
> current (same PID) shell.
Why is "same PID" a requirement? Why isn't something like this
sufficient?
history_f() (
$ history |wc - $HISTFILE|sed \$d
7622 75741 532254 -
14973 29625 320996 /home/jidanni/.bash_history_jidanni
Works as expected.
$ (a=~/.bash_history_jidanni-emacs; HISTFILE=$a history |wc - $a|sed \$d)
7625 75780 532531 - ### I expected to see about 1399/2 here.
13993535
On Sun, Dec 01, 2024 at 10:36:53 +0800, Dan Jacobson wrote:
> $ history |wc - $HISTFILE|sed \$d
>7622 75741 532254 -
> 14973 29625 320996 /home/jidanni/.bash_history_jidanni
> Works as expected.
So, you have 7622 lines of history in memory, and 14973 lines in
that file.
> $ (a=~/.bash
On 11/22/24 4:32 PM, G. Branden Robinson wrote:
Hi Chet,
I should note that I have further patches in preparation to make
parallel changes to the man pages. I meant to hold this one back until
those were ready.
Send whatever you have when you're ready. I will apply where necessary.
--
``The
On 11/29/24 8:05 PM, Dan Jacobson wrote:
$ history
is nice, but what if you want to have it read from a different file?
Use `history -r'?
$ help history
says
If FILENAME is given, it is used as the history file. Otherwise,
if HISTFILE has a value, that is used, else ~/.bash_history
