diff options
| author | Théo Zimmermann | 2017-08-12 01:41:40 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-08-12 01:41:40 +0200 |
| commit | 6548d0c05bc7874ac652ad430b0139860a89c551 (patch) | |
| tree | 71c9829d50f54aa91f87e1ec7f40409667aba6cd /API | |
| parent | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff) | |
More portable location for the time command.
On NixOS in particular, /usr/bin/time doesn't exist.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions