Tell me more ×
Unix & Linux Stack Exchange is a question and answer site for users of Linux, FreeBSD and other Un*x-like operating systems.. It's 100% free, no registration required.
up vote 1 down vote favorite

How would you change the output of the time command from:

real    0m12.304s
user    0m10.187s
sys     0m1.699s

To:

12.30s

EDIT: Using bash (OSX)

share|improve this question
That's a question that's easily answered by looking at the manual of your shell (at least if your shell is zsh, ksh93 or bash). – Stephane Chazelas Oct 30 '12 at 17:45

1 Answer

up vote 6 down vote

Put this in .bashrc: export TIMEFORMAT=%Rs

Then source ~/.bashrc.

Run type time to find out that time is a shell keyword. Then, run man bash (as bash is your shell) and search for "time".

share|improve this answer
3  
If you just want to alter the output for a single invocation: printf "%.2fs\n" $(TIMEFORMAT=%R bash -c 'time ...' 2>&1) – glenn jackman Oct 31 '12 at 0:57

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.