0eaf43a5e1
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.
