Skip to content

docs: Import searchtools.js#13008

Merged
htuch merged 1 commit intoenvoyproxy:masterfrom
dio:import-searchtools
Sep 10, 2020
Merged

docs: Import searchtools.js#13008
htuch merged 1 commit intoenvoyproxy:masterfrom
dio:import-searchtools

Conversation

@dio
Copy link
Member

@dio dio commented Sep 8, 2020

Commit Message: This imports searchtools.js from https://raw.githubusercontent.com/sphinx-doc/sphinx/3.x/sphinx/themes/basic/static/searchtools.js.

Additional Description: #13005 (comment)
Risk Level: None
Testing: CI docs build
Docs Changes: N/A
Release Notes: N/A

Signed-off-by: Dhi Aurrahman dio@tetrate.io

@htuch htuch merged commit f4d21cc into envoyproxy:master Sep 10, 2020
@moderation
Copy link
Contributor

moderation commented Sep 10, 2020

@dio I was wondering if the searchgtools.js is available already as part of the pip3 install for Sphinx - https://github.com/envoyproxy/envoy/blob/master/docs/requirements.txt#L16. A little concerned that as this is a copy paste it could drift and be hard to maintain.

Edit: I just noticed #13005 (comment). Are we trying to override / update an existing version of this file beyond what is in Sphinx 3.2.1?

@dio
Copy link
Member Author

dio commented Sep 10, 2020

@moderation yes, instead of building a full-theme. We override this to introduce small changes to it. I think when we bump (the major version of) Sphinx, that is the time we need to sync.

htuch pushed a commit that referenced this pull request Sep 14, 2020
This adds API version labels to search result items. This overrides the sphinx-docs' searchtools.js.

Depends on: #13008.

Risk Level: Low, cosmetics.
Testing: N/A
Docs Changes: N/A
Release Notes: N/A

Fixes #10311

Signed-off-by: Dhi Aurrahman <dio@tetrate.io>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants