converting the hash tag timestamps in history file to desired string

bash, history, ssh, time-format, unix

Solution

Interesting question: I have tried it but found no simple and clean solution to access the history in a non-interactive shell. However, the format of the history file is simple, and you can write a script to parse it. The following python script might be interesting. Invoke it with `ssh -i private_key user@ip 'path/to/script.py .bash_history'`:

#! /usr/bin/env python3

import re
import sys
import time

if __name__ == '__main__':
    pattern = re.compile(br'^#(\d+)$')
    out = sys.stdout.buffer
    for pathname in sys.argv[1:]:
        with open(pathname, 'rb') as f:
            for line in f:
                timestamp = 0
                while line.startswith(b'#'):
                    match = pattern.match(line)
                    if match: timestamp, = map(int, match.groups())
                    line = next(f)
                out.write(time.strftime('%F %T ', time.localtime(timestamp)).encode('ascii'))
                out.write(line)

Problem

when i store the output of history command via ssh in a file i get something like this ``` ssh -i private_key user@ip 'export HISTFILE=~/.bash_history; export HISTTIMEFORMAT="%D-%T "; set -o history; history' > myfile.txt ``` OUTPUT ``` #1337431451 command ``` as far as ive learnt this hash string represents a timestamp. how do i change this to a string of my desired format P.S- using history in ssh is not outputting with timestamps. Tried almost everything. So i guess the next best thing to do would be to convert these # timestamps to a readable date time format myself. How do i go about it?

Original source