diff options
Diffstat (limited to 'bench/bench.sh')
| -rw-r--r-- | bench/bench.sh | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/bench/bench.sh b/bench/bench.sh index e4b5511..cf1ae49 100644 --- a/bench/bench.sh +++ b/bench/bench.sh @@ -221,7 +221,8 @@ setup() { fi echo "Building bfs ..." - as-user make -s -j"$nproc" release all + as-user ./configure --enable-release + as-user make -s -j"$nproc" all as-user mkdir -p bench/corpus @@ -253,7 +254,12 @@ setup() { echo "Building bfs $commit ..." cd "$worktree" as-user git checkout -qd "$commit" -- - as-user make -s -j"$nproc" release + if [ -e configure ]; then + as-user ./configure --enable-release + as-user make -s -j"$nproc" + else + as-user make -s -j"$nproc" release + fi if [ -e ./bin/bfs ]; then as-user cp ./bin/bfs "$bin/bfs-$commit" else |