Lean4 file icon

Stream: new members

[Asei Inoue]

When I open a directory containing .lean files in an editor such as VSCode, I find it sad that there are no icons.

Do you plan to provide icons for .lean files?

[Sky Wilshaw]

I don't know about official support, but you can get this behaviour with an icon file of your own using an extension like <https://marketplace.visualstudio.com/items?itemName=PKief.material-icon-theme>.

[Asei Inoue]

I want an official icon.

[Bolton Bailey]

I agree. Seems like the new lean-fro website's favicon could be a good option?

(https://lean-lang.org/static/favicon-dark.ico)