feature request: configurable history timestamps

[Alex Shinn]

Hi,

I had initially been confused by the HISTTIMEFORMAT
variable thinking it could be used to change what was
written to the history file, rather than the output of the
history command.

Obviously it would have to be a separate variable, but
the ability to add extra info to the history file would be
very useful to me.  Given the pid and pwd you can
effectively track sessions, and know where you invoked
a command in addition to when.

As a simple change, just statically appending the bash
pid such that the history file looks like:

  #1323582935 217
  command

would enable constructing a session and inferring the
pwd by checking for cd/pushd/popd commands (assuming
no other aliases or scripts are used to chdir).

Note as a hack I've tried using a trap DEBUG to call
out to sed and add this info to the penultimate line of
.bash_history (race conditions shouldn't be a problem if
only one human is using the same account), but as the
history file grows very large this can cause a visible lag.
Alternately I could write a special-purpose command
which jumps directly to the end of the file, but it would
be really nice if bash just did this for you.

Thanks,

-- 
Alex