Convert time with AWK

Hi All,
I need your help with the following:
My input shows the time in this format 1311547776493
I need to convert it (as part of my AWK script) into this format:
18-08-2011 09:35:11.072

Thanks a lot!
Royi

what format is this? how do you end up with this format?

try this command:

date "+%D %H:%M:%S"

Its called unix time :slight_smile: Unix time - Wikipedia, the free encyclopedia

1311547776493

---------- Post updated at 04:14 PM ---------- Previous update was at 04:13 PM ----------

hmm.. just noticed.. unix time is 10 digit only... :frowning:

echo $TIMESTAMP | awk '{print strftime("%c", $0)}'

or

date -d @$TIMESTAMP

where timestamp is the unix time.