diff options
Diffstat (limited to 'bench')
| -rw-r--r-- | bench/bench.sh | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/bench/bench.sh b/bench/bench.sh index ab56b79..0dfd7c4 100644 --- a/bench/bench.sh +++ b/bench/bench.sh @@ -228,7 +228,11 @@ setup() { cd "$worktree" as-user git checkout -qd "$commit" -- as-user make -s -j"$nproc" release - as-user cp ./bin/bfs "$bin/bfs-$commit" + if [ -e ./bin/bfs ]; then + as-user cp ./bin/bfs "$bin/bfs-$commit" + else + as-user cp ./bfs "$bin/bfs-$commit" + fi as-user make -s clean ) done |