Ekdohibs/camlboot
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add script for computing timings

Browse Source
This commit is contained in:
Nathanaël Courant 2021-02-17 14:50:04 +01:00
parent 5c53d505c1
commit dc70540748
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
timed.sh Executable file
View File

@ -0,0 +1,6 @@
#!/usr/bin/env bash
r=$(dirname $0)
echo >> "$r/timings"
echo "$@" >> "$r/timings"
{ time { "$@" 2>&3; }; } 3>&2 2>> "$r/timings"