-
Notifications
You must be signed in to change notification settings - Fork 20
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
Style: make <, ≤, >, ≥ looks better by removing links #20
Style: make <, ≤, >, ≥ looks better by removing links #20
Conversation
Guessed that it could create some issues, here's another patch which
makes things a bit different, it still gives us links in hypothesis AFAIK.
As order stuff has rarely hypothesis but most stuff seems to be in
implications, etc.
Let me know how it goes. :)
…--
Ryan
On May 16 2020, at 3:52 am, Bryan Gin-ge Chen ***@***.***> wrote:
Here's a screenshot of what things look like after your change:
One thing I don't like is that in hx : is_integral α x, I can't tell
that is_integral is a ilnk and that hx, α and x are not. Could you
tweak the colors or some other feature to make the links stand out somehow?
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub, or unsubscribe.
[ { ***@***.***": "http://schema.org", ***@***.***": "EmailMessage",
"potentialAction": { ***@***.***": "ViewAction", "target":
"#20 (comment)",
"url":
"#20 (comment)",
"name": "View Pull Request" }, "description": "View this Pull Request
on GitHub", "publisher": { ***@***.***": "Organization", "name": "GitHub",
"url": "https://github.com" } } ]
|
Hmm, I actually kind of liked it more with all underlines removed by default, since they overlap with the underscores. Could you somehow make it so the non-links are more grayed out or less bold or something? In your dark theme, I like the fact that for the second declaration Sorry for being picky! |
We can definitely do something like this, I'll do it tomorrow, if that's okay.
That's actually a side effect of a CSS filter from my GPU… :'D (I use the Dark Reader extension with Filter+).
Don't worry, it's all about the user experience. |
Now I realize that links in the |
Please make follow-up PRs if you like something else. But if we don't merge something now, then this will never be fixed. |
Those are only enabled upon hovering on them.