Skip to content

More search feature #45

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

Merged
merged 7 commits into from
Apr 1, 2025
Merged

More search feature #45

merged 7 commits into from
Apr 1, 2025

Conversation

xvw
Copy link
Member

@xvw xvw commented Mar 31, 2025

Search by type and polarity to find definitions or declarations

@xvw xvw requested a review from voodoos March 31, 2025 15:12
@xvw xvw force-pushed the add-locate-ident branch from 13e3fd7 to 70b7e77 Compare March 31, 2025 15:24
Copy link
Member

@voodoos voodoos left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did not review the implementation in depth but that seems reasonable to me.

@xvw xvw merged commit 049449a into main Apr 1, 2025
5 checks passed
@xvw xvw deleted the add-locate-ident branch April 1, 2025 16:05
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.

2 participants