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.

Sign up for GitHub

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

Jump to bottom

Use Enso Font in new GUI #8485

Closed
Tracked by #7685
farmaazon opened this issue Dec 7, 2023 · 1 comment · Fixed by #8499
Closed
Tracked by #7685

Use Enso Font in new GUI #8485

farmaazon opened this issue Dec 7, 2023 · 1 comment · Fixed by #8499
Assignees
@somebody1234
Labels
-gui d-easy Difficulty: little prior knowledge required p-medium Should be completed in the next few sprints

Comments

@farmaazon
Copy link
Contributor

farmaazon commented Dec 7, 2023 •
edited
Loading

As in title. The fonts are defined in https://github.com/enso-org/font repository. They should be downloaded during npm install and ready to use in new GUI codebase. For details, see #7197.
@github-project-automation github-project-automation bot moved this to ❓New in Issues Board Dec 7, 2023
@farmaazon farmaazon mentioned this issue Dec 7, 2023
Closed
@farmaazon farmaazon added d-easy Difficulty: little prior knowledge required p-medium Should be completed in the next few sprints -gui labels Dec 7, 2023
@farmaazon farmaazon changed the title Use Enso Font Use Enso Font in new GUI Dec 7, 2023
@farmaazon farmaazon moved this from ❓New to 📤 Backlog in Issues Board Dec 7, 2023
@somebody1234
Copy link
Contributor

somebody1234 commented Dec 7, 2023 •
edited
Loading

Ideally we should also remember to also use this font in:

  • the Code Editor (I think it is currently using the system default monospace font so it looks pretty bad on Windows)
  • certain visualizations (probably JSON, potentially SQL if it is supposed to be monospace)

@somebody1234 somebody1234 mentioned this issue Dec 8, 2023
Merged
5 tasks
@somebody1234 somebody1234 self-assigned this Dec 8, 2023
@farmaazon farmaazon moved this from 📤 Backlog to 👁️ Code review in Issues Board Dec 8, 2023
@mergify mergify bot closed this as completed in #8499 Dec 8, 2023
mergify bot pushed a commit that referenced this issue Dec 8, 2023
@somebody1234
Use Enso font (#8499)
777ae9a 
- Closes #8485

# Important Notes
None
@github-project-automation github-project-automation bot moved this from 👁️ Code review to 🟢 Accepted in Issues Board Dec 8, 2023
@farmaazon farmaazon moved this from 🟢 Accepted to 🗄️ Archived in Issues Board Dec 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@somebody1234 somebody1234

Labels
-gui d-easy Difficulty: little prior knowledge required p-medium Should be completed in the next few sprints
Projects
Issues Board
Archived in project
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Use Enso font enso-org/enso
2 participants
@farmaazon @somebody1234