child time accounting is different from other shells

[Vincent Lefevre <vincent@xxxxxxxxxx>]

With all shells I could test except zsh,

  time sh -c 'pi 500000 > /dev/null & sleep 2'

where "pi 500000 > /dev/null" lasts for less than 2 seconds
(or replace it with any command that takes CPU time less than
2 seconds), includes the time taken by this child process in
the user/system times, but not with zsh:

xvii% time sh -c 'pi 500000 > /dev/null & sleep 2'
sh -c 'pi 500000 > /dev/null & sleep 2'  1.16s user 0.02s system 58% cpu 2.017 total
xvii% time zsh -c 'pi 500000 > /dev/null & sleep 2'
zsh -c 'pi 500000 > /dev/null & sleep 2'  0.00s user 0.00s system 0% cpu 2.023 total

Is this a bug? Shouldn't this behavior be changed to make zsh
consistent with the other shells?

-- 
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)