[docs] [issue23613] searchindex.js is annoying

[Antoine Pitrou]

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"?

----------

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