On Tue, May 01, 2012 at 10:04:47PM -0400, Phillip Susi wrote:
> Note that you need to explicitly specify /usr/bin/time to prevent the
> shell builtin time command from being used, which is more limited.

Or 'command time'.

-- 
Colin Watson                                       [cjwat...@ubuntu.com]

-- 
Ubuntu-devel-discuss mailing list
Ubuntu-devel-discuss@lists.ubuntu.com
Modify settings or unsubscribe at: 
https://lists.ubuntu.com/mailman/listinfo/ubuntu-devel-discuss

Reply via email to