[docs] [issue23613] searchindex.js is annoying

Martin Panter report at bugs.python.org
Sun Mar 8 23:54:12 CET 2015

Martin Panter added the comment:

My own one-liner kicking around in my Bash history that uses GNU Grep options to avoid specific files and directories:

grep -r . --exclude-dir={.git,.hg} --exclude={refcounts.dat,"*.js"} -nIwe PIPE_MAX_SIZE

nosy: +vadmium

Python tracker <report at bugs.python.org>

More information about the docs mailing list