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

move preferences from language server category to spring category #970

Closed
martinlippert opened this issue Feb 8, 2023 · 1 comment
Closed
Assignees
Labels
for: eclipse something that is specific for Eclipse type: enhancement

Comments

@martinlippert
Copy link
Member

In Eclipse, we still have all the language-server related preferences showing up in the preferences in a deep hierarchy below the language server category. This is somewhat hard to find for users (and more an implementation detail of the internal architecture that some parts of the spring tooling are implemented as part of a language server).

Therefore we should move all preferences to the Spring category and have them all show up there, independent whether they are coming from the language server or not.

@martinlippert martinlippert added type: enhancement for: eclipse something that is specific for Eclipse labels Feb 8, 2023
@martinlippert martinlippert added this to the 4.18.0.RELEASE milestone Feb 8, 2023
@BoykoAlex
Copy link
Contributor

Fixed with 63b321a

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
for: eclipse something that is specific for Eclipse type: enhancement
Projects
None yet
Development

No branches or pull requests

2 participants