Skip to content
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

Add favicons #881

Merged
merged 1 commit into from
Oct 23, 2023
Merged

Add favicons #881

merged 1 commit into from
Oct 23, 2023

Conversation

VojtechStep
Copy link
Collaborator

@VojtechStep VojtechStep commented Oct 23, 2023

This PR adds Trebor's simplified Agda logo as favicons, adapting to dark and light themes of the browser.

Fixes #872

@EgbertRijke EgbertRijke merged commit e1e045f into UniMath:master Oct 23, 2023
4 checks passed
@fredrik-bakke
Copy link
Collaborator

Absolutely marvelous! Thanks for taking the initiative to make this small but awesome change

@fredrik-bakke fredrik-bakke added enhancement New feature or request website labels Oct 23, 2023
@EgbertRijke
Copy link
Collaborator

Btw where is this favicon supposed to show? I tried to look for it, but I can't find it anywhere.

@VojtechStep
Copy link
Collaborator Author

It's the image used for the tab icon in browsers, and once search engines reindex the website (which takes some time to happen), it will also appear next to the search results on e.g. Google or DDG.

image

@EgbertRijke
Copy link
Collaborator

For me it doesn't work

@EgbertRijke
Copy link
Collaborator

I still get:

Screenshot 2023-10-24 at 14 34 36

even after restarting my browser

@VojtechStep
Copy link
Collaborator Author

That, uh, shouldn't happen? Did you try refreshing the tab? I was under the impression that modern Safari tries a little harder not to invent their own things that go counter to the rest of the web ecosystem.

@EgbertRijke
Copy link
Collaborator

Yep, tried everything

@fredrik-bakke
Copy link
Collaborator

For reference, I tried viewing the site in Safari too, and I got the same behavior as Egbert.

@VojtechStep
Copy link
Collaborator Author

Smh

@VojtechStep VojtechStep deleted the feature/favicon branch January 21, 2024 16:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request website
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add a favicon
3 participants