Changes
1 changed files (+1/-0)
-
-
@@ -11,6 +11,7 @@"window.customTitleBarVisibility": "never", "window.titleBarStyle": "native", // https://lean-lang.org/documentation/semantic-tokens/ // "The colors in this example are not meant to be nice" "editor.semanticTokenColorCustomizations": { "rules": {"function": "#ff0000", "property": "#00ff00", "variable": "#ff77ff"} },
-