Skip to content
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.

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

[MRG] debug documentation search #453

Merged
merged 1 commit into from
Apr 7, 2023
Merged

[MRG] debug documentation search #453

merged 1 commit into from
Apr 7, 2023

Conversation

rflamary
Copy link
Collaborator

@rflamary rflamary commented Apr 7, 2023

Types of changes

fix doc search with trick from:
readthedocs/sphinx_rtd_theme#1452

Motivation and context / Related issue

How has this been tested (if it applies)

PR checklist

  • I have read the CONTRIBUTING document.
  • The documentation is up-to-date with the changes I made (check build artifacts).
  • All tests passed, and additional code has been covered with new tests.
  • I have added the PR and Issue fix to the RELEASES.md file.

@codecov
Copy link

codecov bot commented Apr 7, 2023

Codecov Report

Merging #453 (0802d87) into master (89f1613) will not change coverage.
The diff coverage is 100.00%.

Additional details and impacted files
@@           Coverage Diff           @@
##           master     #453   +/-   ##
=======================================
  Coverage   94.92%   94.92%           
=======================================
  Files          31       31           
  Lines        6879     6879           
=======================================
  Hits         6530     6530           
  Misses        349      349           

@rflamary rflamary merged commit 2bbfbbb into master Apr 7, 2023
@rflamary rflamary deleted the jquerybug branch August 2, 2023 14:03
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.

1 participant