VSCode has a convention where some variables, like ${userHome}, can be substituted in some settings. But the feature is not a universal feature of settings - it looks like it's implemented on certain fields only. See here.
This would be useful for VDM VSCode in many of the settings we define.
VSCode has a convention where some variables, like ${userHome}, can be substituted in some settings. But the feature is not a universal feature of settings - it looks like it's implemented on certain fields only. See here.
This would be useful for VDM VSCode in many of the settings we define.