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.

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 HTML Search #10604

Merged
merged 4 commits into from Jul 18, 2022
Merged

Fix HTML Search #10604

merged 4 commits into from Jul 18, 2022

Conversation

tk0miya
Copy link
Member

@tk0miya tk0miya commented Jun 26, 2022

Feature or Bugfix

  • Bugfix

Purpose

  • HTML Search: HTML tags are displayed as a part of object name
  • HTML Search: search snipets should not be folded
  • HTML Search: The markers for header links are shown in the search result
  • HTML Search: Minor errors are emitted on fetching search snipets

@tk0miya tk0miya added this to the 5.1.0 milestone Jun 26, 2022
@tk0miya
Copy link
Member Author

tk0miya commented Jun 26, 2022

I noticed this is almost duplicated with #10548.

@AA-Turner
Copy link
Member

Is there anything this PR included that wasn't in #10548?

A

@tk0miya
Copy link
Member Author

tk0miya commented Jul 18, 2022

This changes are still needed. So I rebased this into the HEAD of 5.x now. Merging.

@tk0miya tk0miya merged commit eb5a441 into 5.x Jul 18, 2022
@tk0miya tk0miya deleted the fix_search branch July 18, 2022 14:19
@github-actions github-actions bot locked as resolved and limited conversation to collaborators Aug 18, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
html search type:bug
Projects
None yet
Milestone
5.1.0
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@tk0miya @AA-Turner