diff --git a/tools/unix/clean_indexes.sh b/tools/unix/clean_indexes.sh new file mode 100755 index 0000000000..1752e4bbe3 --- /dev/null +++ b/tools/unix/clean_indexes.sh @@ -0,0 +1,7 @@ +#!/bin/bash +# Removes indices after an app run. You can pass a path as the first argument. +set -u -x +TARGET="${1:-$(dirname "$0")/../../data}" +for mwm in "$TARGET/"*.mwm; do + rm -rf "$TARGET/$(basename "$mwm" .mwm)" +done