[docs] [issue23613] searchindex.js is annoying

[Martin Panter]

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>
<http://bugs.python.org/issue23613>
_______________________________________