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.

Sign up for GitHub

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

Jump to bottom

Add a specific `xml.java.home` preference #145

Closed

fbricon opened this issue May 24, 2019 · 0 comments · Fixed by #147

Assignees

Labels

Milestone

Collaborator

fbricon commented May 24, 2019

currently, the XML language server falls back to the "java.home" preference to launch.
This causes 2 issues:

when the Java extension is not installed, the "java.home" preference is unknown, see Unknown Configuration setting #135
you can't use a JRE to launch the server, as the Java extension doesn't support it, see JRE support #136

Introducing new "xml.java.home" preference which would be checked before "java.home", would solve #135 and help finalizing #136

fbricon added the enhancement label

fbricon assigned xorye

fbricon added this to the v0.7.0 milestone

fbricon mentioned this issue

Unknown Configuration setting #135

Closed

xorye mentioned this issue

Add xml.java.home preference #147

Merged

fbricon closed this as completed in #147

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment