diff --git a/tools/delete-ignored-files.sh b/tools/delete-ignored-files.sh new file mode 100755 index 000000000..19c8545e0 --- /dev/null +++ b/tools/delete-ignored-files.sh @@ -0,0 +1,7 @@ +#!/bin/bash -ex + +# This script assumes that Git is installed + +# The following deletes all files and directories which are ignored by `.gitignore` + +git clean -dfX