Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix search on readthedocs.org (agda#6821)
This addresses a regression in `sphinx_rtd_theme` that causes `sphinxcontrib.jquery` to be not loaded. Consequently, the search page seems to be hanging; the cause is that `jQuery` is undefined. Adding `sphinxcontrib.jquery` is a suggested workaround at readthedocs/sphinx_rtd_theme#1452. Since I see another problem with search locally and in the PR build on rtd.org, I bump to the latest `Sphinx` and `sphinx_rtd_theme`. This doesn't fix the problem, though. However, rtd.org seems to be fine with these requirements. The problem I have been seeing is a `undefined` sprinkled in the `requestUrl` variable in Sphinx's `searchtools.js` which causes page loads to fail for previewing the search hits. Maybe this problem will disappear in the regular build on rtd.org. Squashed commits: * Fix search on readthedocs.org by bumping sphinx_rtd_theme to 1.2.2 1.2.2 includes PR 1448 which fixes issue 1452 - readthedocs/sphinx_rtd_theme#1448 - readthedocs/sphinx_rtd_theme#1452 * Fixup: remove `html_theme_path` Suggested in readthedocs/sphinx_rtd_theme#1452 (comment) * Fixup 2: or, add 'sphinxcontrib.jquery' to 'extensions' * Fixup 3: bump to latest Sphinx and rtd theme
- Loading branch information