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

Search by description produces misleading results #215

Open
expln opened this issue Nov 5, 2024 · 0 comments · Fixed by #221
Open

Search by description produces misleading results #215

expln opened this issue Nov 5, 2024 · 0 comments · Fixed by #221
Labels
bug Something isn't working ready-on-dev

Comments

@expln
Copy link
Owner

expln commented Nov 5, 2024 •
edited
Loading

Search by description currently works by checking if the provided text is a substring of the description of a frame (case insensitively). But descriptions of some frames contain more whitespaces when they are in the source file (due to formatting) than when displayed in the explorer. For example:

image

image

That's why search by description doesn't work sometimes:

image
@expln expln added the bug Something isn't working label Nov 5, 2024
expln pushed a commit that referenced this issue Dec 9, 2024
Fix the bug #215 "Search by description produces misleading results".
2fcd4dd
@expln expln linked a pull request Dec 15, 2024 that will close this issue
Multiple editors #221
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working ready-on-dev
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Multiple editors expln/metamath-lamp
1 participant
@expln