The 'time' reserved word seems to be unable to time subshells that run 'exec'. Is this intentional? (ksh93, mksh and zsh all do manage this.)
$ time (sleep 1) real 0m1,003s user 0m0,001s sys 0m0,002s $ time (exec sleep 1) $ time (echo hi; exec sleep 1) hi $ echo "$BASH_VERSION" 4.4.12(3)-release - Martijn
