-
Hi, I am trying to set a server property equivalent to
metals_config.init_options = {
serverProperties = {
["metals"] = {
["bloop-port"] = 8000,
}
},
}, or just as one key in the metals_config.init_options = {
serverProperties = {
["metals.bloop-port"] = 8000,
},
},
|
Beta Was this translation helpful? Give feedback.
Answered by
ckipp01
Dec 20, 2022
Replies: 1 comment 1 reply
-
Hey @trmckay metals_config = {
serverProperties = {
"-Dmetals.bloop-port=8000",
},
}, Also, this setting is sort of hidden primarily because it's rarely ever used. I've actually never seen someone ask about it. What's your use case here that you want to manually set this? |
Beta Was this translation helpful? Give feedback.
1 reply
Answer selected by
trmckay
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hey @trmckay
serverProperties
isn't nested inside ofinit_options
, it's just inside of the config table. So it'd be like:Also, this setting is sort of hidden primarily because it's rarely ever used. I've actually never seen someone ask about it. What's your use case here that you want to manually set this?