-
-
Notifications
You must be signed in to change notification settings - Fork 141
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
Searching in index #565
Comments
Not just To properly implement this feature, we can:
What do you think @sebastinas ? |
This could re-use the existing integration for the search command, but no idea how much work that is. |
It would be awesome to have search functionality similar to
/
available in the index.By accident I sometimes make a "doubleclick"
<Mouse3>
in the index, after which typing seems to trigger some kind of "search" functionality. Seems kinda strange, since it isn't documented, coudn't find any further information, and also works only if the given index entry starts with the given search prompt.Seems to me like a useful thing to have, maybe even some kind of fuzzy matching would be sometimes desirable.
The text was updated successfully, but these errors were encountered: