Skip to content
  • rtoy's avatar
    Replace $TIMER with time, everywhere. · 49329301
    rtoy authored
    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?)
    49329301