GitLab

This cuts the make startup time by about 30 seconds.  Python is faster
than bash in this case, and also we can now supply multiple directories
to prune, and skip the .repo directory, which is, uh, big.

This is from my mac laptop:

$ time build/tools/findleaves.sh --prune="./out" . Android.mk > /dev/null

real    0m29.186s
user    0m0.550s
sys 0m5.897s

$ time build/tools/findleaves.py --prune="./out" . Android.mk > /dev/null

real    0m4.701s
user    0m0.645s
sys 0m1.294s

$ time build/tools/findleaves.py --prune="./out" --prune="./.repo" . Android.mk > /dev/null
real    0m0.176s
user    0m0.094s
sys 0m0.080s