-
Notifications
You must be signed in to change notification settings - Fork 285
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: add Lean language #1509
base: main
Are you sure you want to change the base?
feat: add Lean language #1509
Conversation
Closes o2sh#1354.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I appreciate the creativity for this art!
While it looks fine in my terminal, it looks misaligned in GitHub. Looks like GitHub's monospace font doesn't play nicely with these characters (it improved when I forced GitHub to use my preferred monospace font). This makes me think that other monospace fonts that users might use won't have good compatibility with this art's characters. How do you feel about simplifying the art (∃
-> E
, etc.)?
Right. I assume GitH*b's monospace font is lacking those Unicode characters, and so a non-monospace fallback font is used. This could indeed also happen on terminals emulators whose monospace fonts collectively do not cover such characters. I am not just using "E" for |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
Thanks a lot for your contribution @foxyseta I've adjusted your ASCII art to better resemble the original logo What do you think?
|
Love it. You're so artsy😍 |
Closes #1354.