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

Preferences quick filtering for available docsets #644

Open
a-b opened this issue Jun 28, 2017 · 3 comments
Open

Preferences quick filtering for available docsets #644

a-b opened this issue Jun 28, 2017 · 3 comments
Labels

Comments

@a-b
Copy link

a-b commented Jun 28, 2017

To improve docset management experience I'm recommending consider adding a quick filter.

@Thibaut
Copy link
Member

Thibaut commented Jun 30, 2017

What do you mean by "quick filter"?

@j-f1
Copy link
Contributor

j-f1 commented Jun 30, 2017

Currently, when you’re looking for docs to enable, you have to scroll through the list. It would be much easier if there was a textbox to filter the docset names to find the one you want.

@Thibaut
Copy link
Member

Thibaut commented Jun 30, 2017

Right. All the docs are indexed and can be enabled in the main search:

devdocs api documentation 2017-06-30 16-34-51

Adding another search on the preference page would be a lot of work. I'm not sure it's worth it.

@Thibaut Thibaut added the feature label Dec 3, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

3 participants