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