clean possible previously existing becnhmark.log

diff --git a/the-big-benchmark.sh b/the-big-benchmark.sh
index 253b74740ab685c290aa8bc303b0e6027cb3feb0..3ce087ff77c5d596b8324c6178a2f34b45cac579 100755 (executable)
--- a/the-big-benchmark.sh
+++ b/the-big-benchmark.sh
@@ -25,6 +25,7 @@ while :; do
 done
 
 set -x
+rm -f data/benchmark.log
 ./all clean --reclone
 ./all compile -r
 ./all run -nohome -benchmarkruns 3 -benchmark demos/the-big-keybench.dem +//div0-stable
@@ -46,6 +47,6 @@ echo " - graphics card (which vendor, which model)"
 echo " - operating system (including whether it is 32bit or 64bit)"
 echo " - graphics driver version"
 echo " - the following info:"
-tail -n 6 data/benchmark.log
+cat data/benchmark.log
 echo
 echo "Thank you"