the-big-benchmark: more detail

diff --git a/the-big-benchmark.sh b/the-big-benchmark.sh
index 15b78e0d93562ac2996c074462e8cb80c0d7be61..1744a1adc2523457ea90858c9512ce97287ea96b 100755 (executable)
--- a/the-big-benchmark.sh
+++ b/the-big-benchmark.sh
@@ -37,7 +37,7 @@ USE_GDB=no ./all run "$@" -nohome -benchmarkruns 3 -benchmark demos/the-big-keyb
        git checkout div0-stable-pred3d9 || git checkout -t origin/div0-stable-pred3d9 || exit 1
 )
 ./all compile -r
-USE_GDB=no ./all run "$@" -nohome -benchmarkruns 3 -benchmark demos/the-big-keybench.dem +//master || true
+USE_GDB=no ./all run "$@" -nohome -benchmarkruns 3 -benchmark demos/the-big-keybench.dem +//div0-stable-pred3d9 || true
 ./all clean -r -f -u
 set +x