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 correct "minus" unicode char for keyboard shortcut hints #3053

Closed
martenbjork opened this issue Aug 21, 2023 · 1 comment
Closed

Use correct "minus" unicode char for keyboard shortcut hints #3053

martenbjork opened this issue Aug 21, 2023 · 1 comment
Assignees
@abey79
Labels
ui concerns graphical user interface

Comments

@martenbjork
Copy link
Contributor

martenbjork commented Aug 21, 2023 •
edited
Loading

Similar to #2862. For shortcuts like ⌘ –, we should use the proper minus character, −.

Before:

+
- (too small, misaligned)

After:

+
− (wider, behaves more like a monospace font)

Bonus: Welcome to the fun world of dashes:

Image
@martenbjork martenbjork added the ui concerns graphical user interface label Aug 21, 2023
emilk added a commit to emilk/egui that referenced this issue Aug 22, 2023
@emilk
Use the minus character instead of "dash"
32b38bb 
See rerun-io/rerun#3053
@emilk emilk mentioned this issue Aug 22, 2023
Merged
@emilk
Copy link
Member

emilk commented Aug 22, 2023

Will be closed by emilk/egui#3271

@emilk emilk closed this as completed Aug 22, 2023
emilk added a commit to emilk/egui that referenced this issue Aug 22, 2023
@emilk
Use the minus character instead of "dash" (#3271)
ec506c0 
* Use the minus character instead of "dash"

See rerun-io/rerun#3053

* docstring

* fix
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@abey79 abey79

Labels
ui concerns graphical user interface
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@martenbjork @emilk @abey79