Unix & Linux Stack Exchange is a question and answer site for users of Linux, FreeBSD and other Un*x-like operating systems. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

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



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). – Stéphane Chazelas Oct 30 '12 at 17:45
up vote 7 down vote accepted

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
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


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.