Skip to content

Commit df5cd40

Browse files
authored
feat: add file icons for .lean files (#749)
1 parent 26448b7 commit df5cd40

File tree

3 files changed

+5
-1
lines changed

3 files changed

+5
-1
lines changed
1.48 KB
Loading
1.46 KB
Loading

vscode-lean4/package.json

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -789,7 +789,11 @@
789789
"configuration": "./language-configuration.json",
790790
"extensions": [
791791
".lean"
792-
]
792+
],
793+
"icon": {
794+
"dark": "./media/lean-file-icon-dark.png",
795+
"light": "./media/lean-file-icon-light.png"
796+
}
793797
},
794798
{
795799
"id": "lean",

0 commit comments

Comments
 (0)