[gambit-list] Re: running remote jobs with `time'