Zsh Mailing List Archive
Messages sorted by: Reverse Date, Date, Thread, Author

Merging extended history (Was: purpose of storing command duration in history)



Peter Stephenson wrote:

> > On 18/03/2025 20:53 GMT Christoph Groth <christoph@xxxxxxxxxxxxxx> wrote:
> >
> > Zsh’s extended history format allows to store the duration of
> > commands in history.  Just curious: how is this useful?  It seems to
> > be useful, because there exist specific options like
> > INC_APPEND_HISTORY_TIME.
>
> Nothing very secret here, I don't think.  It's useful to look and see
> if you're running a command that takes a long time --- for example,
> building firmware --- how long it took last time you ran it, so you
> can go and have a coffee.  Other beverages are available.
>
> As you are probably aware, the extended history format is itself
> optional.

Thanks!  I’m working on a tool for three-way-merging extended zsh
history, and for this the extended format with its timestamps is useful.
(And it’s required for setopt SHARE_HISTORY anyway.)

That’s how I got interested in the “elapsed seconds” field.  In
particular because it’s zero for most commands in my case (I’m not using
INC_APPEND_HISTORY_TIME.)  I was wondering if I’m missing something
useful here.

The merging tool will allow me to sync histories across boxes (using
unison in my case).  I’m a bit puzzled that no one seems to have
developed such a tool so far!

Christoph





Messages sorted by: Reverse Date, Date, Thread, Author