keep local branches alive when running clean

diff --git a/misc/tools/the-big-benchmark/the-big-benchmark.sh b/misc/tools/the-big-benchmark/the-big-benchmark.sh
index 667e413f3f6d158cafaf7ec019f0e22d069d6864..b67015cbb412cfa34335c19c5922cb7581abdc33 100755 (executable)
--- a/misc/tools/the-big-benchmark/the-big-benchmark.sh
+++ b/misc/tools/the-big-benchmark/the-big-benchmark.sh
@@ -12,7 +12,8 @@ echo " ================="
 echo
 if [ -f ./all ]; then
        echo "WARNING: running this script will destroy ANY local changes you"
-       echo "might have on the repository that haven't been pushed yet."
+       echo "might have on the repository that haven't been pushed or stored"
+       echo "in a local branch yet."
        echo
        if [ x"$1" != x"--yes" ]; then
                echo "Are you absolutely sure you want to run this?"
@@ -34,7 +35,7 @@ if [ -f ./all ]; then
 fi
 
 if [ -f ./all ]; then
-       ./all clean --reclone
+       ./all clean -fU -m -r
        ./all compile -r
        export USE_GDB=no
        set -- ./all run "$@"
@@ -70,7 +71,7 @@ for e in omg low med normal high ultra ultimate; do
        cat data/benchmark.log >> data/the-big-benchmark.log
 done
 if [ -f ./all ]; then
-       ./all clean -r -f -u
+       ./all clean -r
 fi
 
 rm -f data/benchmark.log