my $time = `/bin/sh -c 'time ...'`;