UCSD-PL / vscode

Visual Studio Code
https://code.visualstudio.com
MIT License
0 stars 7 forks source link

migrate editor config in settings.json to default config for the editor #14

Closed rlisahuang closed 1 year ago

rlisahuang commented 1 year ago

We have configuration for the editor and projection boxes locally in .vscode/settings.json, but the configuration is not part of the monaco editor build for the web version. We should hard-code configuration critical for the tool on the editor instance through VSCode's API.

Important config: