Set the correct unicode character for "ctrl" shortcuts#3186

Merged

Wumpf merged 1 commit intoemilk:masterfrom rerun-io:antoine/fix-ctrl-char

Jul 28, 2023

+3-3

Commits on Jul 28, 2023

Set the correct unicode character for "ctrl" shortcuts
abey79
committed