Replace $TIMER with time, everywhere.
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?)
Loading
Please register or sign in to comment
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?)