Changes
1 changed files (+5/-5)
-
-
@@ -1,4 +1,9 @@{ // 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"} }, "editor.wordWrap": "on", // This is what everyone else does "files.insertFinalNewline": true,
-
@@ -10,9 +15,4 @@// Make title bar consistent with other apps in KDE "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"} }, }
-