[docs] [issue23613] searchindex.js is annoying
report at bugs.python.org
Sun Mar 8 21:06:32 CET 2015
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
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".
Python tracker <report at bugs.python.org>
More information about the docs