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

Improve preferences and extension manager #749

Open
smathot opened this issue Feb 8, 2021 · 0 comments
Open

Improve preferences and extension manager #749

smathot opened this issue Feb 8, 2021 · 0 comments
Assignees

Comments

@smathot
Copy link
Collaborator

smathot commented Feb 8, 2021

The Preferences and the Plug-in and extension manager aren't very user friendly, in part because they lack search functionality. Three ways to improve this:

  • Add a search bar to both options. For the preferences the search should apply to the labels, frame headers, and config values. For the extension manager, the search should apply to the names, descriptions, and values (authors, etc.)
  • In the extension manager, there should be a button to open the preferences specifically for that extension.
  • The extension manager should look nicer.
@smathot smathot self-assigned this Feb 8, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant