Respect global settings in settings.json, then the local ones in launch.json

[scholarsmate]

Port 9000 is the default port for the Ωedit server that powers the Data Editor. The problem is that I have another service that is running on port 9000, so I need to change the port that the Ωedit server runs on. I want to use port 9001 for that. I think the most intuitive place to persist that variable is in a global settings.json that is configurable at the extension level.

Clicking on Edit in settings.json allows me to change the port, but that setting seems to be ignored. It would be good to have that work as it will allow users to configure a different port and use the Data Editor without requiring a .vscode/launch.json in their repository.

The workaround for now is to set the port in launch.json like so:

           "dataEditor": {
                "port": 9001,
                "logging": {
                    "file": "${workspaceFolder}/dataEditor-${omegaEditPort}.log",
                    "level": "info"
                }
            },

Having it respect the global settings, then allow them to be overridden in a local launch.json would be better.