add note about settings

hhu-adam · Aug 1, 2024 · 0cb4edc · 0cb4edc
1 parent 1f9ba51
commit 0cb4edc
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/demo/src/App.tsx b/demo/src/App.tsx
@@ -4,7 +4,13 @@ import LeanMonacoComponent from './LeanMonaco'
 import { LeanMonacoOptions } from 'lean4monaco'
 
 function App() {
-  const [options, setOptions] = useState<LeanMonacoOptions>({websocket: {url: 'ws://localhost:8080/'}, vscode: {"workbench.colorTheme": "Visual Studio Light"}})
+  const [options, setOptions] = useState<LeanMonacoOptions>({websocket: {url: 'ws://localhost:8080/'}, vscode: {
+    "workbench.colorTheme": "Visual Studio Light",
+    /* To add settings here, you can open your settings in VSCode (Ctrl+,), search
+     * for the desired setting, select "Copy Setting as JSON" from the "More Actions"
+     * menu next to the selected setting, and paste the copied string here.
+     */
+  }})
   const [numberEditors, setNumberEditors] = useState(1)
 
   return (