Requested by Stelian Ionescu to support Gentoo. Some Gentoo systems don't have /usr/bin/time. (What kind of Unix system doesn't have /usr/bin/time?)