Current version of xgboost.readthedocs.io has a broken search box.
Enabling themes on ReadTheDocs is known to break the search function, as
reported in
[this document](https://github.com/rtfd/readthedocs.org/issues/1487). To get
around the bug, we replace the `searchtools.js` file with our custom version.
