[docs] [issue23613] searchindex.js is annoying

[Marc-Andre Lemburg]

Marc-Andre Lemburg added the comment:

On 08.03.2015 20:57, Antoine Pitrou wrote:
> 
> Antoine Pitrou added the comment:
> 
>> Well, that's not useful in a generated file.
> 
> Well, here's a case where it's useful... Asking me to change tools is quite obvious and quite pointless at the same time. How about we respond to all Windows-specific issues with "switch to Linux"?

Georg suggested excluding the file from your search. That's a very
reasonable answer.

You don't have to change your tools for this,
just configure them to not look in .js files or perhaps not look
in this particular file if it returns false positives for you.

I'd suggest to close this as "wont fix".

----------
nosy: +lemburg

_______________________________________
Python tracker <report at bugs.python.org>
<http://bugs.python.org/issue23613>
_______________________________________