New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix documentation search #1201

Merged

JonnyWong16 merged 1 commit into pkkid:master from JonnyWong16:bugfix/docs

Aug 2, 2023

Collaborator

JonnyWong16 commented Aug 1, 2023

Description

Fixes jQuery error in documentation search.

Fixes #1200

Ref: readthedocs/sphinx_rtd_theme#1434

Type of change

Please delete options that are not relevant.

Bug fix (non-breaking change which fixes an issue)
This change requires a documentation update

Checklist:

My code follows the style guidelines of this project
I have performed a self-review of my own code
I have commented my code, particularly in hard-to-understand areas
I have added or updated the docstring for new or existing methods
I have added tests when applicable


          Fix docs search

1e9c546

JonnyWong16 merged commit a7d29a3 into pkkid:master

3 checks passed

JonnyWong16 deleted the bugfix/docs branch

August 2, 2023 20:44

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet