Done in r4835.
Time would be shown as:
Total time: 0:00:12.947s
Also note that time not be printed, if process was terminated by OS or by user.
In fact Evgeny, as we always display the number of hours and minutes, I guess it would be better to display :
Total time : 0h 3mn 12.947s
Leading zeros removed in r4848
So values will look like (fully consistent with a format in Maven):