CRBS / cdeep3m

Please go to https://github.com/CRBS/cdeep3m2 for most recent version
Other
58 stars 10 forks source link

/usr/bin/time not available on all systems #56

Closed coleslaw481 closed 5 years ago

coleslaw481 commented 5 years ago

Not all systems have time installed or in /usr/bin for that matter so it might be a good idea to remove the /usr/bin prefix and have the user update their path or add a parameter to the .sh scripts which lets the user set the time command used with the default set to just time