[bug] times builtin output wrong

[Stephane Chazelas <stephane.chazelas@xxxxxxxxx>]

$ times
0m3.36s 0m1.95s
0m12.23s 0m0.15s
$ time
shell  2.02s user 1.17s system 1% cpu 3:36.66 total
children  7.34s user 0.10s system 3% cpu 3:36.66 total
$ echo $((7.34*100/60))
12.233333333333333

It looks like they're expressed in 60/100th of seconds.

The code has:

/* display a time, provided in units of 1/60s, as minutes and seconds */
#define pttime(X) printf("%ldm%ld.%02lds",((long) (X))/3600,\
                         ((long) (X))/60%60,((long) (X))*100/60%100)

So it kind of assumes the times are in 1/60s but they're not, they're in clock
ticks.

The "time" output is correct though.

-- 
Stephane